RETROSPECTIVE: The Design and Implementation of a Certifying Compiler

Optimizing compilers continue to be critical tools in all software development processes. Even more than in 1998 when this paper first appeared, production-quality compilers have become so complex that they defy any attempt at formal verification. Compilers are debugged using large numbers of test cases, some of which are distilled at considerable expense from large application programs. Besides being expensive and time-consuming, the effectiveness of testing is reduced by the practical impossibility of adequately covering the execution paths of the compiled programs. In this paper we proposed a technique for checking the result of each compilation instead of verifying the compiler’s source code. This was inspired in part by the technique of run-time result checking [14] and the observation that it is often easier to check the output of a program than to verif