A formally verified compiler ensures that compilation does not introduce any bugs in programs. In the CompCert C compiler, this correctness property requires reasoning about realistic languages by using a semantic framework. This invited talk explains how this framework has been effectively used to turn CompCert from a prototype in a lab into a real-world compiler.

I am professor professor of computer science at the University of Rennes. My research interests include semantics, theorem proving, static analysis, verified compilation and software security.