A Certifying Code Generation Phase

Guaranteeing correctness of compilation is a vital precondition for correct software. Code generation can be one of the most error-prone tasks in a compiler. One way to achieve trusted compilation is certifying compilation. A certifying compiler generates for each run a proof that it has performed the compilation run correctly. The proof is checked in a separate theorem prover. If the theorem prover is content with the proof one can be sure that the compiler produced correct code. This paper reports on the construction of a certifying code generation phase for a compiler. It is part of a larger project aimed at guaranteeing the correctness of a complete compiler. We emphasize on demonstrating the feasibility of the certifying compilation approach to code generation and focus on the implementation and practical issues. It turns out that the checking of the certificates is the actual bottleneck of certifying compilation. We present a proof schema to overcome this bottleneck. Hence we show the applicability of the certifying compilation approach for small sized programs processed by a compiler's code generation phase.