Universität Karlsruhe
An Architecture for Verified Compiler Construction

Technischer Bericht

[GGGHZ:97]Thilo Gaul, Gerhard Goos, Andreas Heberle, Wolf Zimmermann, Wolfgang Goerigk, An Architecture for Verified Compiler Construction, Jan 1997.


Verified compilers are essential for the development of safety-critical software systems. Critical parts of control systems are yet often written and verified on the assembler level because compilers for high-level languages are not considered trustworthy. For industrial application the techniques for the construction of correct compilers must be easy to apply and must be integrated in the software development process. This raises not only verification problems on the algorithmic level but also architectural problems of constructing a verified compiler according to current software engineering standards. In this paper we show that specification and verification can be integrated in the traditional architecture of a compiler. This integration reduces the complexity as well as the size of the verification.

[Erzeuge bibTeX Eintrag]




Prof. Gerhard Goos
Prof. Wolf Zimmermann
Dr. Thilo Gaul
Dr. Andreas Heberle
Dr. Wolfgang Goerigk