This paper reports on a non-trivial case-study carried out in the context on the German correct compiler construction project Verifix. The PVS system is here used as a vehicle to formally represent and verify a generic checker routine (run-time result verification) used in compiler back-ends. The checker verifies the results of a sophisticated labeling process of intermediate language expression trees with instances of compilation rule schemata. Starting from an operational specification (i.e. a set of recursive PVS functions), necessary declarative properties of the checker are formally stated and proved correct.

Online Copy

Postscript (141 KB).

BibTeX Entry

@InProceedings{DV:99, author = "Axel Dold and Vincent Vialard", title = "Formal Verification of a Compiler Back-end Generic Checker Program", series = "Lecture Notes in Computer Science", number = "1755", pages = "470-480", booktitle = "Proc. of the Andrei Ershov Third International Conference Perspectives of System Informatics (PSI'99)" year = 2000, publisher = "Springer-Verlag" }