|[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