Blech, Jan OlafGlesner, SabineDadam, PeterReichert, Manfred2019-10-112019-10-1120043-88579-380-6https://dl.gi.de/handle/20.500.12116/28810Optimizations 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.enText/Conference Paper1617-5468