Universitšt Karlsruhe
Construction of Verified Compiler Front-Ends with Program-Checking
  author={Andreas Heberle and Thilo Gaul and Wolf Zimmermann},
  title=\{Construction of Verified Compiler Front-Ends with Program-Checking},
  booktitle=\{Proceedings of PSI '99},
  pages=\{481 ff.},
  abstract=\{This paper describes how program-checking can be used to establish the   correctness of a compiler front-end which was generated by unverified   compiler construction tools. The basic idea of program-checking is   to use an unverified algorithm whose results are checked by a   verified component at run time. The approach not only simplifies the   construction of a verified compiler front-end because checking the   result of the analysis is much simpler to verify than the   verification of a high sophisticated compiler front-end. It even   allows to define a notion of front-end correctness. Furthermore, we   are still able to use existing generators tools without major   modifications.  Additionally, this work points out the tasks which   still have to be verified and it discusses the flexibility of the   approach. },
  series=\{Lecture Notes in Computer Science},
  address=\{Novosibirsk, Russia},