How to provide proof that software is bug-free? Verified compilation to the rescue
Event details
Date | 27.02.2024 |
Hour | 11:15 › 12:15 |
Speaker | Professor Sandrine Blazy (IRISA) |
Location | |
Category | Conferences - Seminars |
Event Language | English |
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
Practical information
- General public
- Free
Organizer
- Professor Clément Pit-Claudel