Paper Info
Title
Formal Verification of Transformations for Peephole Optimization
Abstract
. In this paper we describe a formal verification of transformationsfor peephole optimization using the PVS system [12]. Our basicapproach is to develop a generic scheme to mechanize these kinds of verificationsfor a large class of machine architectures. This generic scheme isinstantiated with a formalization of a non-trivial stack machine [14] anda PDP-11 like two-address machine [2], and we prove the correctness ofmore than 100 published peephole optimization rules for these...
Year
DOI
Venue
1997
10.1007/3-540-63533-5_24
FME
Keywords
Field
DocType
reu- sability of specifications.,higher-order logic,transformations,peephole optimization,formal verification,pv system,higher order logic
Programming language,Peephole,Computer science,Correctness,Formal specification,Theoretical computer science,Peephole optimization,Stack machine,Higher-order logic,Formal verification
Conference
ISBN
Citations 
PageRank 
3-540-63533-5
4
0.99
References 
Authors
13
4
Name
Order
Citations
PageRank
Axel Dold1658.44
Friedrich W. Von Henke242549.05
Holger Pfeifer317912.77
Harald Rueß452638.69