When applying formal methods to critical software, it is generally the source code that is certified. Compiler bugs can therefore invalidate the certification. It is not uncommon, in industry, to carry manual code reviews of the assembly code produced by the compiler to establish the absence of compiler-induced bugs.

Several approaches have been considered to remedy this situation, such as proof-carrying code and translation validation. The most obvious approach is the certification of the compiler itself, viewed as an ordinary program: prove (on machine) that the machine code produced by the compiler has the same semantics as the source program.

In this talk, I will present ongoing work on the certification (in the Coq proof assistant) of a realistic, moderately-optimizing compiler of the kind used for embedded programming (from a subset of the C language to PowerPC assembly code). The first results obtained include the specification of the semantics for several intermediate languages, as well as the proof of correctness of several optimisations based on dataflow analyses.