Vous êtes ici

Formal verification and design of static analyses

Equipe et encadrants
Département / Equipe: 
Site Web Equipe: 
Directeur de thèse
David Pichardie
Co-directeur(s), co-encadrant(s)
NomAdresse e-mailTéléphone
David Pichardie
02 99 84 22 59
Sujet de thèse

The IRISA/Inria Celtique group has several open PhD positions. These positions are funded by David Pichardie's european ERC VESTA project (2018-2023). PhD applicants must have a Master in Computer Science.

We seek candidates with a solid theoretical background in Computer Science, in at least one of the following topics: 

  • Formal semantics of programming languages
  • Compiler implementation
  • Abstract interpretation
  • Coq proof assistant

Potential research projects:

  • Verification of static analysis with the Coq proof assistant
  • Formal verification and synthesis of abstract interpreters using the Galois connection framework
  • Formal verification of state-of-the-art SSA-based compiler optimisations
  • Advanced abstract interpretation for software security (Java, C, or assembly programs)
  • Innovative techniques for extraction of efficient code with Coq

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, pages 247--259. ACM Press, 2015.

Gilles Barthe, Delphine Demange, and David Pichardie. Formal verification of an SSA-based middle-end for compcert. ACM Trans. Program. Lang. Syst. (TOPLAS), 36(1):4, 2014.



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