In this article, we describe a framework for formally verifying the correctness of compiler optimizations. We begin by giving formal semantics to a variation of the TRANS language [6], which is designed to express optimizations as transformations on control-flow graphs using temporal logic side conditions. We then formalize the idea of correctness of a TRANS optimization, and prove general lemmas about correctness that can form the basis of a proof of correctness for a particular optimization. We present an implementation of the framework in Isabelle, and as a proof of concept, demonstrate a proof of correctness of an algorithm for converting programs into static single assignment form. © 2010 Springer-Verlag.
CITATION STYLE
Mansky, W., & Gunter, E. (2010). A framework for formal verification of compiler optimizations. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6172 LNCS, pp. 371–386). https://doi.org/10.1007/978-3-642-14052-5_26
Mendeley helps you to discover research relevant for your work.