Universitšt Karlsruhe
Construction of Verified Compiler Front-Ends with Program-Checking

Conference Article

[1]Andreas Heberle, Thilo Gaul, Wolf Zimmermann, Construction of Verified Compiler Front-Ends with Program-Checking, Proceedings of PSI '99, p. 481 ff., Springer, Jul 1999.


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.

[Generate bibTeX entry]


Prof. Wolf Zimmermann
Dr. Thilo Gaul
Dr. Andreas Heberle