Formal Verification of Transformations for Peephole Optimizatio

Published in the Proceedings of the 4th International Symposium of Formal Methods Europe (FME'97) , Graz, 1997.

---

Authors

Axel Dold, F.W. von Henke, Holger Pfeifer, Harald Rueß

Abstract

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.

gzipped postscript or postscript

BibTeX Entry

@InProceedings{DHPR97,
  author =       "A. Dold and F.W. von Henke and H. Pfeifer and H. Rue{\ss}",
  title =        "Formal Verification of Transformations for Peephole Optimization",
  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
}

---

PVS Theories

---

Harald Ruess: ruess@csl.sri.com