Can you trust your compiler? Can we make sure that the generated machine code behaves as prescribed by the semantics of the source program? This question is particularly acute for critical software that has been certified by applying formal methods to its source code: any bug in the compiler can invalidate the guarantees obtained by formal verification of the source.

Several approaches to this problem have been proposed: proof-carrying code, translation validation, and compiler verification. In the latter approach, mechanized program proof is applied to the compiler itself to prove a semantic preservation result between the source and generated codes.

In the context of the CompCert project (http://compcert.inria.fr/), I am working on such a semantic preservation proof, mechanized using the Coq proof assistant, for a realistic, moderately-optimizing compiler translating a subset of the C language down to PowerPC assembly code. An originality of this work is that most of the compiler is programmed directly in the specification language of Coq (a small pure functional language), then automatically extracted to executable Caml code.

The seminar will give a general overview of the CompCert compiler and its (rather large) proof of correctness, and outline some directions for future work on verification of other tools that participate in the development and verification of critical software.