Preuve de programmes

Mots-clés

logiques de programme
méthodes algorithmiques de vérification

Axis 1: Foundations and spreading of deductive program verification

Members: S. Boldo, S. Conchon, J.-C. Filliâtre, C. Marché, G. Melquiond, A. Paskevich, B. Wolff

This axis covers the subject of "deductive verification" from the point of view of its foundations but also our will to spread its use in software development. The general motto we want to defend is “deductive verification for the masses”. A non-exhaustive list of subjects we want to address is as follows.

The verification of general-purpose algorithms and data structures: the challenge is to discover adequate invariants to obtain a proof, in the most automatic way as possible, in the continuation of the current VOCaL project and various case studies.
Uniform approaches to obtain correct-by-construction programs and libraries, in particular by automatic extraction of executable code (in OCaml, C, CakeML, etc.) from verified programs, and including innovative general methods like advanced ghost code, ghost monitoring, etc.
Automated reasoning dedicated to deductive verification, so as to improve proof automation; improved combination of interactive provers and fully automated ones, proof by reflection.
Improved feedback in case of proof failures: based on generation of counterexamples, or symbolic execution, or possibly randomized techniques à la quickcheck.
Seamless Integration of "deductive verification" into interactive theorem proving systems in order to allow a smooth transition from interactive to automated proofs, and refinements from high-level algorithms to efficient code.
Reduction of the trusted computing base in our toolchains: production of certificates from automatic proofs, for goal transformations (like those done by Why3), and from the generation of VCs

Software: Why3, Isabelle/C + Backends

Axis 2: Reasoning on mutable memory in program verification

Members: S. Conchon, J.-C. Filliâtre, J.-H. Jourdan, C. Marché, G. Melquiond, A. Paskevich, M. Sighireanu

This axis concerns specifically the techniques for reasoning on programs where aliasing is the central issue. It covers the methods based on type-based alias analysis and related memory models, on specific program logics such as separation logics, and extended model-checking. It concerns the application on analysis of C or C++ codes, on Ada codes involving pointers, but also concurrent programs in general. The main topics planned are:

The study of advanced type systems dedicated to verification, for controlling aliasing, and their use for obtaining easier-to-prove verification conditions. Modern typing system in the style of Rust, involving ownership and borrowing, will be considered.
The design of front-ends of Why3 for the proofs of programs where aliasing cannot be fully controlled statically, via adequate memory models, aiming in particular at extraction to C; and also for concurrent programs.
The continuation of fruitful work on concurrent parameterized systems, and its corresponding specific SMT-based model-checking.
Concurrent programming on weak memory models, on one hand as an extension of parameterized systems above, but also in the specific context of multicore OCaml.
In particular in the context of the ProofInUse joint lab, design methods for Ada, C, C++ or Java using memory models involving fine-grain analysis of pointers. Rust programs could be considered as well.

Software: Cubicle

Axis 3: Preuve de programmes orientés données

Members: V. Benzaken, É. Contejean

We propose to prove that database updates performed by data-oriented languages effectively preserve the invariants of these databases. Starting from the semantics of SQL formalized in Coq by Benzaken and Contejean, our first study involves relational systems, most commonly used today. Our further objective is to extend our approach to the NoSQL-style languages.

Axis 4: Deductive verification for systems

Members: I. Aït Sadoun, F. Boulanger, S. Taha, B. Wolff, L. Ye

This axis deals with the verification of properties of systems that are not necessary modeled using a general purpose programming language. The main activities are: 1. defining modeling tools to describe systems and their properties in a way that allows the use of deductive verification. 2. providing algorithms to translate the model of a system and its properties towards a deductive logic framework.

Examples:

Isabelle/HOL theory of CSP, to prove properties on concurrent systems (Safouan, Lina, Burkhart)
Isabelle/HOL semantics of TESL, to check temporal properties of systems (Frédéric, Burkhart)
Isabelle_C and combinations to process specifications in CSP, TESL, LTL, ... (Safouan, Frederic, Burkhart)
Formal model of human behaviors, to prove properties of systems that include humans (Safouan, Frédéric, Valentin Fouillard)
Isabelle/HOL theory of Dwyer's patterns, to check temporal logic properties of systems (Safouan)
Formal models of ontologies to check the consistency of specifications during the overall design of a system (Idir, Burkhart)
Event-B semantics of Composition operators/BPEL/OWL-S, to check behavioural and functional properties of systems (Idir)

Software: OntoEventB Rodin plugin, TESL