Verified compilation: towards zero-defect software
1 : Univ Rennes, Inria, CNRS, IRISA
Univ Rennes, Inria, CNRS, IRISA F-35000 Rennes
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.
More generally, this approach opens the way to the verification of software tools involved in the production and verification of software.
| Type : | : | typedoc |
| Langue du texte intégral | : | anglais |
| Date de production, écriture | : | 25/06/2025 |
| Thématiques | : | Keynote - Sandrine Blazy |
| PDF version | : |  PDF version |
- Poster
