Universität Karlsruhe
A Formal Correctness Proof for Code Generation from SSA Form in Isabelle/HOL
@conference{,
  author={Jan Olaf Blech and Sabine Glesner},
  title=\{A Formal Correctness Proof for Code Generation from SSA Form 
in Isabelle/HOL},
  booktitle=\{Proceedings der 3. Arbeitstagung Programmiersprachen (ATPS) auf der 34. Jahrestagung der Gesellschaft fĂĽr Informatik},
  year=\{2004},
  month=\{September},
  publisher=\{Lecture Notes in Informatics},
  abstract=\{Optimizations in compilers are the most error-prone phases in the
compilation process. Since correct compilers are a vital precondition
for software correctness, it is necessary to prove their
correctness. We develop a formal semantics for static
single assignment (SSA) intermediate representations and prove
formally within the Isabelle/HOL theorem prover that a relatively
simple form of code generation preserves the semantics of the
transformed programs in SSA form. This formal correctness proof does
not only verify the correctness of a certain class of code generation
algorithms but also gives us a sufficient, easily checkable
correctness criterion characterizing correct compilation results
obtained from implementations (compilers) of these algorithms.},
  url=\{http://www.info.uni-karlsruhe.de/papers/Blech-Glesner-ATPS-2004.pdf},
}

Login
Links