© Jean-Claude Moschetti / CNRS Photothèque
Unifying Speaker Sandrine Blazy
Sandrine Blazy is professor at the University of Rennes and deputy director of the IRISA laboratory. Her research interests include verified compilation, formal semantics, deductive verification, static analysis and software security. In 2004, she spent two sabbatical years at Inria Paris, where she joined Xavier Leroy to start working on what would become CompCert, the first formally verified compiler for the C language. Since then, CompCert has won several awards, including the La Recherche award in information sciences (2011), the ACM software system award (2021), the ACM SIGPLAN Programming Languages Software Award (2022) and the Lucas award from FME board (2023). Sandrine Blazy received in 2023 the CNRS silver medal. Her research work aim of providing CompCert with more compilation possibilities and stronger formal guarantees.
Talk
From Operational Semantics to Verified Compilation: Mechanized Reasoning on Realistic Languages in the CompCert Compiler
Tuesday, 9:00
Room: Europe A
A formally verified compiler ensures that compilation does not introduce any bugs in programs. This correctness property requires reasoning about the languages of the compiler. This talk will present the semantic framework that was designed in the CompCert C compiler for reasoning on realistic languages. In addition, this framework was used to provide CompCert with more compilation opportunities and to offer additional guarantees in terms of software security.