Jacques-Henri Jourdan


CV: English - Francais


Email

jacques-henri.jourdan [at] lri [dot] fr

My PGP public key

Mail address

LMF, Bat 650
Univerité Paris Saclay
91405 Orsay Cedex
France

Physical address

LMF - Bât.650, bureau 63
1, rue Raimond Castaing
91190 Gif-sur-Yvette
France

Welcome !

I am a CNRS researcher (chargé de recherche CNRS) in Formal Methods Laboratory (LMF) of Université Paris Saclay. My research interests belong to the formal verification of software and to the design and development of programming languages.

Before integrating that team,

  • I was a postdoc at Max Plank Institute for Software Systems (MPI-SWS) in Derek Dreyer's team, on the RustBelt project. Our objective was to formalize the soundness of Rust's type system and prove that some particular Rust libraries written using unsafe features do not break the whole type system;
  • I was a PhD student in computer science at Inria, in team Gallium, under the direction of Xavier Leroy. I designed, developed and formally verified Verasco, a static analyzer based on abstract interpretation. I defended successfully on 26th May 2016. My PhD thesis is available here. It received the 2016 thesis prize of the GdR GPL (french research group on programming and software engineering)!

Research interests

I am interested in the formal verification of software, using different approaches:

  • Xavier Denis, my PhD student, is developing Creusot under my supervision a deductive verification tool for the Rust programming language.
  • I participated to the development of the Iris concurrent separation logic, within the Coq proof assistant.
  • I participated to the development of two logics based on Iris for proving concurrent programs with a weakly consistent memory semantics. The first one, iRC11, targets the C11 memory model. In addition, Glen Mével my PhD student, developed Cosmo, which targets the Multicore OCaml memory model.
  • Together with collaborators, I used some of these logics to build semantic models of the type system of Rust: in a sequentially consistent setting, in a weakly consistent setting, or for proving the correctness a type-directed weakest-precondition computation.
  • During my PhD thesis, together with my collaborators, I used Coq to code and prove correct Verasco, a static analyzer based on abstract interpretation. The program was written directly in the calculus of construction and transformed into OCaml through Coq's extraction mechanism.
  • I participated to the development of the formally verified compiler Compcert, by writing its parser and by contributing to its IEEE758-compliant floating-point support.

In addition, I am interested in the design and development of programming languages and their support software:

  • I am member of the development team of the OCaml language. I am particularly interested in the development of the runtime library.
  • I developed a memory profiler for OCaml, which is now integrated in the official OCaml distribution. Its specificity is that it is statistical: it randomly samples a few allocations only in order to make it possible to get precise information on the memory behavior of the program without degrading significantly its performances.
  • I have helped the development of ocaml-interop which makes it possible to interoperate Rust and OCaml code
  • I have developed a parser for the C11 grammar, based on the LR(1) technology. This turned out to be particularly subtle!

Misc

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.