Vous êtes ici

Verified JIT compiler

Equipe et encadrants
Département / Equipe: 
Site Web Equipe: 
Directeur de thèse
David Pichardie
Co-directeur(s), co-encadrant(s)
Sujet de thèse

This position is funded by David Pichardie's european ERC VESTA project (2018-2023), hosted by ENS Rennes.

The goal is to design, implement and formally verify a JIT compiler.



Applicants must have a Master in Computer Science. We seek excellent candidates with a solid background in Computer Science, in all the following topics:

  • formal semantics of programming languages
  • compiler implementation
  • abstract interpretation design and implementation

The position may start September 1st 2019. Applicants should send their curriculum vitae, cover letter and names/contact information of two references to David Pichardie before end of June 2019.


Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie. A formally-verified C static analyzer. In 42nd symposium Principles of Programming Languages (POPL), pages 247--259. ACM Press, 2015

Gilles Barthe, Delphine Demange, David Pichardie. Formal Verification of an SSA-Based Middle-End for CompCert. ACM Trans. Program. Lang. Syst. 36(1): 4:1-4:35 (2014)

Début des travaux: 
IRISA - Campus universitaire de Beaulieu, Rennes