My research interests lie in formal verification and automated reasoning. Together with other members of the Toccata team, I develop Why3, a platform for deductive program verification. Why3 provides a functional language with contracts, called WhyML, and uses third-party theorem provers to discharge verification conditions. WhyML can be compiled to OCaml. It also serves as an intermediate language for verification of C and Ada programs.
Between 2000 and 2008, I took part in the Evidence Algorithm project. We developed a mathematical assistant, called System for Automated Deduction (SAD) and intended for automated verification of formalized mathematical texts. SAD processes texts written in ForTheL, a variant of controlled English language that closely follows the natural language and style of mathematical publications.
In 2008, I contributed to the development of CiME 3, a tool for certification of termination proofs for term rewriting systems and also an automated termination prover.
Here you can find my publications.
I teach a course on Unix system programming (Principes des systèmes d'exploitation, M3101) at the IUT d'Orsay. In preparation of the lecture slides (C), I used materials by Dominique Gouyou-Beauchamps and Lydia Nicaud. The classroom notes (TD and TP) are mostly derived from the system programming course by Cédric Bastoul, to whom I owe the overall presentation and the majority of exercises.
Last update: 22 Mar 2016