A Generic Specification for Verifying Peephole Optimizations

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

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.

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

@TechReport{DHPR95,
  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"
}