Abstract:
We generally take it for granted that a compile generates machine code that behaves as prescribed by the semantics of the source program. However, compilers are complicated pieces of software, and bugs in the compiler sometimes cause it to silently generate incorrect machine code. This is a concern for critical embedded 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, 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 talk 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.
Back to LCTES 2008 Technical Program