Sciweavers

Share
GI
2004
Springer

A Formal Correctness Proof for Code Generation from SSA Form in Isabelle/HOL

9 years 3 months ago
A Formal Correctness Proof for Code Generation from SSA Form in Isabelle/HOL
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. To be published in Proceedings der 3. Arbeitstagung Programmiersprachen (ATPS) auf der 34. Jahrestagung der Gesellschaft f¨ur Informatik, Ulm, Germany, 2004, to appear in Lecture Notes in Informatics.
Jan Olaf Blech, Sabine Glesner
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Where GI
Authors Jan Olaf Blech, Sabine Glesner
Comments (0)
books