Towards Rigorous Compiler Implementation Verification

This paper sketches our approach to rigorously prove the correctness of a compiler executable down to its binary machine code implementation. We will emphasize the central role of partial program correctness and its preservation, which capture the intuitive correctness requirements for transformational programs and in particular for compilers on realistic machines. Vertical and horizontal compositionality of L-simulation (preservation of partial correctness) allows for combining small proof modules to finally complete the entire proof. Although often left out of sight, implementation verification is definitely necessary, not only but also for compiler programs. Modularization makes a rigorous compiler correctness proof also for the final compiler executable possible and feasible. 1 Introduction The purpose of this paper is to show that rigorous verification of compilers down to their machine code implementation is possible and feasible. The key ideas are preservation of partial correc..