Kick-off meeting program

Wednesday 2 November 2011

located in the new PCRI building of the LRI (salle 465, bâtiment 650, rue Noetzlin, Orsay).

9:00 - 9:15 Welcome, Overview of the Day

9:15 - 9:45 Les messages de l’ANR

  Franck Barbier (responsable adjoint du département STIC à l’ANR) Presentation

9:45 - 10h30 The ANR- itp-paral Project - A General Overview

  Burkhart Wolff (LRI, coordinator of the project) Presentation

10:30 - 10:45 Coffee-Break

10:45 - 12:15 Topic 1: Prover Architecture

  Bruno Barras (INRIA Saclay - LIX) Overview of the Prover Architecture Tasks in Paral-ITP

  Makarius Wenzel The parallel prover architecture of Isabelle

  Bruno Barras A Concurrency Model for Coq: Theoretical and Implementation Challenges

12:15 - 13:30 Lunch

13:30 - 15:30 Topic 2: Document Model

  Hugo Herbelin (INRIA Rocquencourt Paris - PPS, Coq’s head developer) Presentation of the Document Model task

  Makarius Wenzel Parallel and asynchronous processing of structured proof documents in Isabelle/Isar

  Yann Régis-Gianas (Université Paris Diderot - PPS)

15:30 - 16:00 Coffee-Break

16:00 - 17:00 Topic 3: Front-end Technologies

  Makarius Wenzel (LRI, Isabelle’s head developer) Front-end technology: prover interaction and integration

17:00 - 17:15 Coffee-Break

17:15 - 18:15 Topic 4: Formal Analysis

  Burkhart Wolff The Role of Formal Analysis in the Paral-ITP Project

  Lukas Brügger (ETH Zürich) Web Service and GUI Testing with HOL-TestGen< (finally absent)

Abstract of talks

Burkhart Wolff, The ANR- itp-paral Project - A General Overview

Interactive theorem proving is a technology of fundamental importance for mathematics and computer-science. It is based on expressive logical foundations and implemented in a highly trustable way. Applications include huge mathematical proofs and semi-automated verifications of complex software systems. Interactive development of larger and larger proofs increases the demand for computing power, which means explicit parallelism on current multicore hardware. The architecture of contemporary interactive provers such as Coq, Isabelle or the HOL family goes back to the influential LCF system (from 1979), which has pioneered key principles like correctness by construction for primitive inferences and definitions, free programmability in userspace via ML, and toplevel command interaction. Both Coq and Isabelle have elaborated the prover architecture over the years, driven by the demands of sophisticated proof procedures, derived specification principles, large theory libraries etc. Despite this success, the operational model of interactive proof checking is largely limited by sequential ML evaluation and the sequential read-eval-print loop, as inherited from LCF. The proposed project intends to overcome the sequential model both for Coq and Isabelle, to make the resources of multi-core hardware available for even larger proof developments. Beyond traditional processing of proof scripts as sequence of proof commands, and batchloading of theory modules, there is a large space of possibilities and challenges for pervasive parallelism. This affects many layers of each prover system: basic computational structures, inference kernel, tactical programming, proof command language, and interactive front-ends.

This talk attempts to present the research problem of the project, its consequences and potential solutions to a wider public interested in one of the foundational areas: logics, theorem proving, parallel computing models, formal methods and software engineering.

Burkhart Wolff The Role of Formal Analysis in the Paral-ITP Project

The Paral-ITP Project aims at the modification of the prover architecture of two major theorem proving systems of the world, which have achieved a remarquable reputation wrt. to logical consistency and system quality. Formal analysis of certain critical parts of the architecture ensures high standards of trustability, in continuation of the qualities of the modest LCF command-line prover. Here we investigate some key aspects like an activity to find a formal kernel model that can be analysed in comparison to classical LCF models, activities to verify persistent algorithms relevant for the efficient treatment of the document model as well as activities to test front-end technologies such as GUI’s (which must run on various platforms) or future Web-Services.

Lukas Brugger Web Service and GUI Testing with HOL-TestGen

In this talk, we present recent work on model-based web service and GUI testing. As many modern, large-scale applications follow the service-oriented architecture paradigm, support for testing service-based applications is of big importance for a model-based testing tool like HOL-TestGen. In more detail, we present how we extended the test driver of HOL-TestGen such that it allows for testing of WSDL compliant web services.

The test driver, which includes the test harness and the generation of test scripts, is written in the F# language allowing full integration into the .net platform, which easily allows for calling web services directly. The generation of test scripts is based on Isabelle’s powerful code generator, which we extended with support for F#.

This document was initially translated from LATEX by HEVEA.