Compiling with proofs
George C. Necula, Peter Lee · 1998
I propose a new compiler architecture for compiling source-level programs into a combination of object code and a proof that the object code preserves certain properties of the source program. Such a certifying compiler is structured as a pipeline of certifying static analyses---analyses that produce an explicit proof of the code properties that they infer---along with certifying code transformations, which transform not only the code but also the input proof to a target proof. The purpose of a certifying compiler is to allow independent and easy verification of the properties of the generated code without the cost of running a program analyzer and without the need to trust such a system. The certifying compiler complements earlier work on Proof-Carrying Code by providing an automatic way to produce the required safety proofs when the safety properties are statically decidable or can be checked at run time. The thesis is that this approach is more practical than approaches based on pro...