|||Jan Olaf Blech, Sabine Glesner, Johannes Leitner, Steffen MĂĽlling, A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL, Proceedings of the COCV-Workshop (Compiler Optimization meets Compiler Verification), 8th European Conferences on Theory and Practice of Software (ETAPS 2005), Elsevier, April 2005.
Correctness of compilers is a vital precondition for the correctness
of the software translated by them. In this paper, we present two
approaches for the formalization of static single assignment (SSA)
form together with two corresponding formal proofs in the Isabelle/HOL
system, each showing the correctness of code generation. Our
comparison between the two proofs shows that it is very important to
find adequate formalizations in formal proofs since they can simplify
the verification task considerably. Our formal correctness proofs do
not only verify the correctness of a certain class of code generation
algorithms but also give us sufficient, easily checkable correctness
criteria characterizing correct compilation results obtained from
implementations (compilers) of these algorithms. These correctness
criteria can be used in a compiler result checker.