I recently finished my PhD thesis:
Certification of a Tool Chain for Deductive Program Verification
The thesis defense will take place on January 14th at 14:00 in CEA-NanoINNOV, Palaiseau.
The thesis consists in a development of a Coq-certified OCaml plug-in for deductive verification of ACSL-annotated C programs in the Frama-C platform. Its source code can be downloaded here.
The jury is composed of:
- Xavier Leroy, Inria Rocquencourt
- Gilles Barthe, IMDEA Software Institute
- Roberto Di Cosmo, Laboratoire PPS, Université Paris Diderot 7
- Emmanuel Ledinot, Dassault Aviation
- Burkhart Wolff, LRI Université Paris-Sud 11
- Claude Marché, Inria Saclay – Île-de-France
- Benjamin Monate, CEA-LIST, Lab. de Sûreté du Logiciel
A new version of my certified verification condition generator is available. Provided that you have Coq (v8.3) installed, you can recheck the proofs, extract and build the code along with the parser and printer and launch the example with
$make -j test-all
Update (22/07): compatibility with why3 0.70
You can download an and try a first version of Whycert, a certified verification condition generator.