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.