University of Ulm, Faculty of Computer Science, Dept. of Artificial Intelligence up: Dept. of AI

Formal Verification of a Compiler Back-end Generic Checker Program

Axel Dold, Vincent Vialard

Proc. of the A. Ershov 3rd Int. Conference Perspectives of System Informatics (PSI'99)
Novosibirsk, Akademgorodok, Russia, July 1999
Springer LNCS 1755
© Springer-Verlag


 Abstract

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"
}


Dept. of AI Homepage Research Help Mail to Webmaster A. Dold - Sept 2, 1999