Abstract
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 production of software. Verifying the compiler itself provides guarantees that no errors are introduced during compilation.
This course first introduces the basics of verified compilation, using the Coq theorem prover. Then, it presents CompCert, a 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.
Course material
- Slides
- Reused Coq developments:
- Benjamin Pierce et. al. Software foundations - volume one: simple imperative programs [Coq module Imp]
- Xavier Leroy. Companion Coq development for the lecture Traduttore, traditore: formal verification of a compiler from the course Mechanized semantics, Collège de France
- IMP toy language [Coq module IMP]
- Library for small-step semantics [Coq module Sequences]
- Library for simulation diagrams [Coq module Simulation]
- VM language, compilation from IMP to VM [Coq module Compil]
- CompCert compiler including some studied parts:
- User's manual
- Observable events
- Tools for small-step semantics
- Observable behaviors of programs
- Memory model used by the semantics of all the languages of the compiler
- CompCert C source language: syntax and semantics
- Animating the CompCert C semantics
- Clight language
- RTL language
- Main correctness theorems and composition of passes
- Blazy, Dargaye, Leroy. Formal verification of a C compiler front-end. FM 2006.
- Blazy, Leroy. Mechanized semantics for the Clight subset of the C language. JAR 2009.
- Leroy. A formally verified compiler back-end, JAR 2009.
- Leroy, Appel, Blazy. Formal verification of a C-like memory model and its uses for verifying program transformations. JAR 2008.
- Leroy, Blazy, Kastner, Schommer, Pister, Ferdinand. CompCert - A formally verified optimizing compiler. ERTS2 2016.
- Kastner, Wunsche, Barrho, Schlickling, Schommer, Schmidt, Ferdinand, Leroy, Blazy. CompCert: Practical experience on integrating and qualifying a formally verified optimizing compiler. ERTS2 2018.
Introductory reading
Leroy. Formal verification of a realistic compiler, Comm. ACM 52(7):107-115, 2009.Further reading