Universitšt Karlsruhe
Mechanized Verification of Compiler Back-Ends
  author={Axel Dold and Thilo Gaul and Wolf Zimmermann},
  title=\{Mechanized Verification of Compiler Back-Ends},
  booktitle=\{Proceedings of  STTT '98},
  abstract=\{  We describe an approach to mechanically prove the correctness of   BURS specifications and show how such a tool can be connected with   BURS based back-end generators [Emmelmann92]. The proofs are   based on the operational semantics of both source and target system   languages specified by means of Abstract State Machines   [Gurevich95]. In [Zimmer-Gaul:97] we decomposed the   correctness condition based on these operational semantics into   local correctness conditions for each BURS rule and showed that   these local correctness conditions can be proven independently.   The specification and verification system PVS is used to   mechanicalyy verify BURS-rules based on formal representations of   the languages involved. In particular, we have defined PVS proof   strategies which enable an automatic verification of the rules.   Using PVS, several erroneous rules have been found. Moreover, from   failed proof attempts we were able to correct them.},