I'm senior researcher at CNRS. I work in the VALS team (LRI, Université Paris Sud & CNRS / INRIA Saclay - Île-de-France). I'm doing research in deductive program verification.

Short bio: I did a PhD from 1995 to 1999 under the supervision of Christine Paulin, regarding verification of imperative programs in the system Coq. Right after my PhD, in fall 1999, I redesigned the architecture of Coq, to isolate a kernel ; this is briefly described in this paper. Then I left for a post-doc at SRI, in the PVS team, where I started the development of the ICS decision procedure. When I returned to France, I started in 2001 the development of a tool for program verification called Why, used for the proof of C programs (in the Caduceus tool, now subsumed by Frama-C) and for the proof of Java programs in the Krakatoa tool. In 2010, the Why tool became Why3.

Publications / Program committees / Doctoral juries


I'm an enthusiastic programmer since 1984 (I was 13). My first computer was a Thomson TO7/70, on which I used to code in Basic and 6809 assembly. In 1986, I switched to an Atari 520 ST, on which I used to code in GFA Basic and in 68000 assembly. In the early 1990s, I progressively moved to PC. Today, I code mostly in OCaml, under Linux. A few years ago, I discovered Project Euler ; if you like mathematics and programming, you'll love it.

I'm the (co)author of the following programs:

Many other libraries and applications on that page dedicated to OCaml programming.


I'm teaching compilers at École Normale Supérieure.

I'm teaching INF411 and INF564 at École Polytechnique.

Older teaching material: