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

Formal Verification of Transformations for Peephole Optimization

A. Dold, F. W. von Henke, H. Pfeifer, H. Rueß

appeared in: Proc. of the 4th Internat. Symposium of Formal Methods Europe (FME'97) , Graz


In this paper we describe a formal verification of transformations for peephole optimization using the PVS system. Our basic approach is to develop a generic scheme to mechanize these kinds of verifications for a large class of machine architectures. This generic scheme is instantiated with a formalization of a non-trivial stack machine and a PDP-11 like two-address machine, and we prove the correctness of more than 100 published peephole optimization rules for these machines. In the course of verifying these transformations we found several errors in published peephole transformation steps. From the information of failed proof attempts, however, we were able to discover strengthened preconditions for correcting the erroneous transformations.

 Online Copy

Available as Postscript (114 KB) or gzipped Postscript (45 KB)

PVS Specification files: peephole.dump or gzipped peephole.dump.gz

 BibTeX Entry
  author =       "A. Dold and F.W. von Henke and H. Pfeifer and H. Rue{\ss}",
  title =        "Formal Verification of Transformations for Peephole
  editor =       "J. Fitzgerald, C.B. Jones, P. Lucas",
  volume =       "1313",
  series =       "Lecture Notes in Computer Science",
  pages =        "459--472",
  booktitle =    "{FME} '97: Formal Methods: Their Industrial Application 
                     and Strengthened Foundations}", 
  year =         1997,
  publisher =    "Springer Verlag",
  month =        September

Dept. of AI Homepage Research Help Mail to Webmaster H. Pfeifer - Mar. 3, 1997