A framework for formal verification of compiler optimizations

Abstract. In this article, we describe a framework for formally verify-ing 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 optimiza-tion. 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. Key words: optimizing compilers, theorem proving, program transfor-mations, temporal logic