It is generally expected that the compiler is semantically
transparent, that is, produces executable code that behaves as
prescribed by the semantics of the source code. However, compilers --
and especially optimizing compilers, which attempt to increase the
efficiency of generated code through program analyses and
transformations -- are highly complex software systems that perform
delicate symbolic computations. Bugs in the compiler are therefore
unavoidable : they can cause wrong code to be produced from a correct
source code
The CompCert project investigates the formal verification
of realistic compilers usable for critical embedded software. Such
verified compilers come with a mathematical, machine-checked proof
that the generated executable code behaves exactly as prescribed by
the semantics of the source program. By ruling out the possibility of
compiler-introduced bugs, verified compilers strengthen the guarantees
that can be obtained by applying formal methods to source programs.
This talk describes the formal verification of compilers and focuses
on two experimentation : the C CompCert compiler and the MLCompCert
compiler. MLCompCert is the mechanically verified compiler for the
purely functional fragment of ML that I have developed and verified
in Coq in my Ph. D. thesis.