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

A Generic Specification for Verifying Peephole Optimizations

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

Technical Report UIB 95-14, Universität Ulm, Fakultät für Informatik, Dec. 1995

Note: This report is superseded by Formal Verification of Transformations for Peephole Optimization.


In this paper a generic specification for verifying local optimizations on machine code (peephole optimization) using the specification and verification system PVS is presented. The scheme which provides useful definitions, basic properties and user-defined proof strategies abstracts from the specific instruction set of a machine as well as from its semantics. In addition, we formally represent a stack machine as well as a two-address machine. The general scheme is applied to both machines and local optimizations are formalized and verified using the defined proof strategies.

 Online Copy

Available as Postscript (189 KB) or compressed Postscript (56 KB)

 BibTeX Entry
  author = "Axel Dold and F.W. von Henke and H. Pfeifer and H. Rue{\ss}",
  title = "A Generic Specification for Verifying Peephole Optimizations",
  institution =  "Universit{\"a}t Ulm, Fakult{\"a}t f{\"u}r Informatik",
  year =         "1995",
  number =       "95-14",
  type = "Ulmer Informatik-Berichte"

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