A formally verified compiler ensures that compilation does not introduce any bugs in programs. Achieving this level of assurance requires reasoning about realistic languages by using a semantic framework. This talk will explain how such a framework has been effectively used to turn the CompCert C compiler from a research prototype into a production tool qualified for safety-critical avionics software. This experience demonstrates how mechanized semantics can serve as a milestone for building trustworthy systems in practice. More broadly, this approach extends beyond compilation, paving the way toward the verification of software tools involved in software production and verification.

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