Gesellschaft fr Informatik e.V.

Lecture Notes in Informatics

Informatik 2004, Informatik verbindet, Band 2, Beiträge der 34. Jahrestagung der Gesellschaft für Informatik e.V. (GI), Ulm, 20.-24. September 2004 P-51, 449-458 (2004).

GI, Gesellschaft für Informatik, Bonn


Peter Dadam, Manfred Reichert (eds.)

Copyright © GI, Gesellschaft für Informatik, Bonn


A formal correctness proof for code generation from SSA form in isabelle/HOL

Jan Olaf Blech and Sabine Glesner


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 Is- abelle/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.

Full Text: PDF

GI, Gesellschaft für Informatik, Bonn
ISBN 3-88579-3080-6

Last changed 24.01.2012 21:47:26