Jean-Baptiste Tristan
Ph.D. student in computer science
INRIA Paris-Rocquencourt
Gallium team
Email: jean-baptiste dot tristan at inria dot fr
CV
I am now working at the Microsft Research & INRIA joint laboratory in the tools for proofs group of Damien Doligez. In a few month, I will be a postdoctoral fellow at Harvard, working with Professor Greg Morrisett.
Research interests
- Formal verification of software using proof assistants.
- Translation validation, proof-carrying code.
- Software fault isolation, binary instrumentation.
- Compilation, program analysis and optimization.
Research projects
- Compcert: formal verification of realistic compilers usable for critical embedded software.
Publications
- Formal verification of translation validators,
Ph.D. dissertation, english version
[pdf]
- A simple, verified validator for software pipelining,
POPL 2010,
with Xavier Leroy.
[pdf]
- Verified Validation of Lazy Code Motion,
PLDI 2009,
with Xavier Leroy.
[pdf]
- Formal verification of translation validators: A case study on instruction scheduling optimizations,
POPL 2008,
with Xavier Leroy.
[pdf]