Formal verification of an optimizing compiler

Programmers naturally expect that compilers and other code generation tools produce executable code that behaves as prescribed by source programs. However, compilers are complex programs that perform many subtle transformations. Bugs in compilers do happen and can lead to silently producing incorrect executable code from a correct source program. This is a significant concern in the context of high-assurance software that has been verified (at the source level) using formal methods (static analysis, model checking, program proof, etc): any bug in the compiler can potentially invalidate the guarantees so painfully established by the use of formal methods. There are several ways to generate confidence in the compilation process, including translation validation and proof-carrying code. This talk focuses on applying program proof technology to the compiler itself, in order to prove a semantic preservation theorem for every pass of the compiler. We present preliminary results from the Compcert experiment: the development and proof of correctness of a moderately-optimizing compiler for a large subset of the C language. The proof of correctness is mechanized using the Coq proof assistant. Moreover, most of the compiler itself is written directly in the functional subset of the Coq specification language, from which executable Caml code is automatically extracted.