The formal verification of compilers
Xavier Leroy
Abstract
Formal semantics of programming languages supports not only reasoning over individual programs (program correctness), but also reasoning over program transformations and static analyses, as typically found in compilers (tool correctness). With the help of a proof assistant, we can prove semantic preservation properties of program transformations and semantic soundness properties of static analyses that greatly increase the confidence we can have in compilers and program verification tools.
The topics covered in this course include:
- Non-optimizing compilation of a structured imperative language to a virtual machine, and its correctness proof.
- Notions of semantic preservation.
- Various forms of operational semantics and their mechanization in Coq: big-step, small-step, small-step with continuations.
- Examples of program optimizations: dead code elimination, register allocation.
- Compiler verification "in the large" : an overview of the
CompCert verified C compiler.
We use the Coq proof assistant and build on the formalization of the IMP language from Logical Foundations by Pierce et al.
Course material
- The videos of the lectures.
- The slides for the lecture.
- Coq development, source distribution: git repository (includes a copy of "Logical Foundations" and other material from the summer school).
- Coq development, commented and pretty-printed for online viewing:
- Semantics: various forms of semantics for IMP.
- Compil: compilation from IMP to a virtual machine, proofs of correctness for this compiler.
- Deadcode: liveness analysis and dead code optimization.
- Regalloc: extension to register allocation.
- Library Sequences: transition sequences and their properties.
- Appendix Fixpoint: computing fixpoints in well-founded lattices, with applications to liveness analysis.
Introductory reading
Xavier.Leroy@inria.fr