jacques-henri.jourdan [at] lri [dot] fr
Before integrating that team,
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...
My PhD thesis is available here. Its title is "Verasco: a Formally Verified C Static Analyzer".
It received the 2016 thesis prize of the GdR GPL (french research group on programming and software engineering)!
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
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.
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.