Skip to content

Thesis Defense

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.


COQ2: Informal Presentation

This is the paper I will present at the Coq Workshop associated with the ITP conference at FLoC 2010.

It is a presentation of the techniques and Coq features I’m applying in my PhD thesis.


MLF-omega: Partial Type Inference with Higher-Order Types

This is my master thesis I did at INRIA Rocquencourt in the équipe Gallium under the supervision of Didier Rémy.


This is not a blog