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 talk explains how this framework has been effectively used to turn CompCert from a prototype in a lab into a real-world compiler, and how this framework opens the way to the trust of other development tools.

I am a professor professor of computer science at the University of Rennes. My research interests focus on the development of trustworthy software using deductive verification