Towards Proof Generating Compilers
Arnd Poetzsch-Heffter, Marek Gawkowski
Technische Universität Kaiserslautern, Germany
Correctness of compilation is important for the reliability of
software. New techniques to guarantee correctness do not verify the
compiler itself, but check for each compiled program whether it is
correctly translated. Following these ideas, we developed an
approach in which checking is realized as proof checking within a
formal specification and verification framework. Based on formal
specifications of source and target language and a translation
predicate, compilers produce, in addition to the target program
c, a proof that c is correct w.r.t. its source program. This proof can be
checked independently of the compiler by the framework.
Thus, it can be used as a translation certificate.
The paper describes the overall approach and applies it to a simple
translation scenario. Specification and verification is done within
the theorem prover Isabelle/HOL. To show the flexibility of the
approach, we present two different proof techniques for translation
correctness.
Keywords: compilation correctness, translation validation, formal translation contract, automatic proof generation, proof checking.