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.

• Type: Conference
• Year: 2004
• Where: GI
• Authors: Jan Olaf Blech, Sabine Glesner
• Keywords: Checkable Correctness Criterion, Correctness, Formal Correctness Proof, GI 2004, Theoretical Computer Science