Jacques-Henri Jourdan

CV: English - Francais


jacques-henri.jourdan [at] normalesup [dot] org

My PGP public key

Address (MPI-SWS)

Jacques-Henri Jourdan
Max Plank Institute for Software Systems (MPI-SWS)
Campus E1 5
D-66123 Saarbrücken

Welcome !

I am currently a postdoc at Max Plank Institute for Software Systems (MPI-SWS) in Derek Dreyer's team, on the RustBelt project. Our objective is to formalize Rust's type system and prove that some particular unsafe Rust code fragments do not break the whole type system

Before my postdoc, I was a PhD student in computer science at Inria, in team Gallium, under the direction of Xavier Leroy. I defended successfully on 26th May 2016.

Research interests

My research interests include formal verification of software. In particular, my PhD project lies exactly between abstract interpretation and the Coq proof assistant.

I am also interested in several subjects linked to programming languages: LR parsing, floating-point arithmetic, compilation...

PhD thesis

My PhD thesis is available here. Its title is "Verasco: a Formally Verified C Static Analyzer".


Vincent Laporte and I are the two main authors of the Verasco formally verified static analyzer. I have written the abstract interpreter, and most of the numerical abstract domain hierarchy.

I developed a statistical memory profiler for OCaml. It provides OCaml developers a flexible tool for understanding the memory behavior of an OCaml program with virtually no overhead. It can be used through the 4.03.0+statistical-memprof Opam switch.

I am an occasional contributor to the CompCert verified compiler. In particular, I am the initial author of its parser, and I contributed to its support of IEEE754-compliant floating-point numbers.

With my wife, we are the authors of a few R packages.


I was the teaching assistant for the course "Langages de programmation et compilation", at ENS with Jean-Christophe Filliâtre, years 2013/2014 and 2014/2015.

I have been one of the organizers of the Junior Seminar of Inria Paris

I am a member of the France-IOI association since a few years now. I used to participate to the organization of the French Bebras contest contest, which aims at popularizing computer science for teenagers.

I have been a member of hackEns, the hackerspace of ENS. I am still happy to do fun hacks with electronics or with my RepRap.