Universität Karlsruhe
Compiler Correctness and Implementation Verification: The Verifix Approach

Technischer Bericht

[Goerigk-et-al:CC96]Wolfgang Goerigk, Axel Dold, Thilo Gaul, Gerhard Goos, Andreas Heberle, Heinrich von Henke, Ulrich Hoffmann, Hans Langmaack, Wolf Zimmermann, Compiler Correctness and Implementation Verification: The Verifix Approach, P. Fritzson (Ed.), Jan 1996 (TR-Nr.: R-96-12).


Compiler correctness is crucial to the software engineering of safety critical software. It depends on both the correctness of the compiling specification and the correctness of the compiler implementation. We will discuss compiler correctness for practically relevant source languages and target machines in order to find an adequate correctness notion for the compiling specification, i.e. for the mapping from source to target programs with respect to their standard semantics, which allows for proving both specification and implementation correctness. We will sketch our approach of proving the correctness of the compiler implementation as a binary machine program, using a special technique of bootstrapping and double checking the results. We will discuss mechanical proof support for both compiling verification and compiler implementation verification in order to make them feasible parts of the software engineering of correct compilers.

[Erzeuge bibTeX Eintrag]




Prof. Gerhard Goos
Prof. Wolf Zimmermann
Dr. Thilo Gaul
Dr. Andreas Heberle
Prof. Hans Langmaack
Prof. Heinrich von Henke
Dr. Axel Dold
Dr. Wolfgang Goerigk
Dr. Ulrich Hoffmann