How to provide proof that software is bug-free? Verified compilation to the rescue
le 11 octobre 2023
13h15Campus de Beaulieu Salle i-50 - bât. 12D
Intervention de Sandrine Blazy professeure à l'Université de Rennes dans l'équipe EPICURE, à l'IRISA, dans le cadre des séminaires du département Informatique.
Deductive verification provides very strong guarantees that software is bug-free. Since the verification is usually done at the source level, the compiler becomes a weak link in the software-production chain. Verifying the compiler itself provides guarantees that no errors are introduced during compilation. This talk will illustrate this approach through CompCert, the first fully verified compiler for C that is actually usable on real source code and that produces decent target code on real-world architectures. More generally, this approach opens the way to the verification of software tools involved in the production and verification of software.
- Thématique(s)
- Formation, Recherche - Valorisation
- Contact
- Killian Barrere
Mise à jour le 29 septembre 2023