Deductive Program Verification
In the past decade, there have been significant advances made in the domain of deductive program verification. They are emphasized by some success stories of application of these techniques on industrial-scale software, e.g. the Atelier B system was used to develop part of the embedded software of the Paris metro line 14 and other railroad-related systems, a formally proved C compiler was developed using the Coq proof assistant, Microsoft's hypervisor for highly secure virtualization was verified using VCC and the Z3 prover, the L4-verified project developed a formally verified micro-kernel with high security guarantees, using analysis tools on top of the Isabelle/HOL proof assistant. Another sign of recent progress is the emergence of deductive verification competitions.
In the deductive verification context, there are two main families of approaches. Methods in the first family build on top of mathematical proof assistants (e.g. Coq, Isabelle) in which both the models and the programs are encoded, and the proofs that a program meets its specification is typically conducted in an interactive way using the underlying proof construction engine. Methods from the second family proceed by the design of standalone tools taking as input a program in a particular programming language (e.g. C, Java) specified with a dedicated annotation language (e.g. ACSL, JML) and automatically producing a set of mathematical formulas (the verification conditions) which are typically proved using automatic provers (e.g. Z3, Alt-Ergo, CVC4).
The first family of approaches usually offers a higher level of assurance than the second, but also demands more work to perform the proofs (because of their interactive nature) and makes them less easy to adopt by industry. The second kind of approaches has benefited in the past years from the tremendous progresses made in SAT and SMT solving techniques, allowing more impact on industrial practices, but suffers from a lower level of trust: in all parts of the proof chain (the model of the input programming language, the VC generator, the back-end automatic prover) potential errors may appear, compromising the guarantee offered.
Finally, recent trends in the industrial practice for development of critical software is to require more and more guarantees of safety, e.g. the upcoming DO-178C standard for developing avionics software adds to the former DO-178B the use of formal models and formal methods. It also emphasizes the need for certification of the analysis tools involved in the process.
We are interested in developing practical tools for verifying high-level programs, in particular data structures and algorithms. Although our tools might target several concrete languages, we use an ML-style language as an intermediate or source language, as we have found this choice to significantly ease the verification process. Our specifications are expressed in a typed extension of first-order logic we designed as a good compromise between expressiveness and a high degree of proof automation.
Our main tool, Why3, is based on the traditional weakest-precondition calculus approach. Why3 leverages SMT solvers for automating proofs, but it is also able to produce proof obligations that can be solved interactively in Coq, Isabelle, or PVS.
Our long-term goal is to decrease the cost of program verification, and to be able to verify larger bodies of code, in particular large collections of reusable libraries of data structures and algorithms. In the short term, we aim to improve the expressiveness of the specification and programming language used by Why3.
- Thibaut Balabonski
- Jean-Christophe Filliâtre
- Quentin Garchery (PhD student)
- Jacques-Henri Jourdan
- Cláudio Lourenço (postdoc)
- Claude Marché
- Guillaume Melquiond
- Andrei Paskevich
Former contributors: Martin Clochard, Léon Gondelman, Arthur Charguéraud, Romain Bardou, François Bobot, Paolo Herms, Johannes Kanig, Kalyan Krishnamani, Asma Tafat.
- ANR Project BWare
- ANR Project U3CAT
- System@tic Project Hi-Lite
- European COST Action FoVeOOS
- RTRA Digiteo Project Hisseo
- Why3: a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs.
- Jean-Christophe Filliâtre. One logic to use them all. In 24th International Conference on Automated Deduction (CADE-24), volume 7898 of Lecture Notes in Artificial Intelligence, pages 1-20, Lake Placid, USA, June 2013. Springer. [ full text on HAL ]
- Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich. The spirit of ghost code. In Armin Biere and Roderick Bloem, editors, 26th International Conference on Computer Aided Verification, volume 8859 of Lecture Notes in Computer Science, pages 1-16, Vienna, Austria, July 2014. Springer. [ full text on HAL | .pdf ]
- Jean-Christophe Filliâtre and Andrei Paskevich. Why3 - where programs meet provers. In Matthias Felleisen and Philippa Gardner, editors, Proceedings of the 22nd European Symposium on Programming, volume 7792 of Lecture Notes in Computer Science, pages 125-128. Springer, March 2013. [ full text on HAL ]