Universität Karlsruhe
An Architecture for Verified Compiler Construction
  author={Thilo Gaul and Gerhard Goos and Andreas Heberle and Wolf Zimmermann and Wolfgang Goerigk},
  title=\{An Architecture for Verified Compiler Construction},
  booktitle=\{Proceedings of Joint Modular Languages
Conference 1997, Poster Session},
  abstract=\{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. },