A framework for formal verification of compiler optimizations

William Mansky, Elsa Gunter

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationInteractive Theorem Proving - First International Conference, ITP 2010, Proceedings
Number of pages16
StatePublished - 2010
Event1st International Conference on Interactive Theorem Proving, ITP 2010 - Edinburgh, United Kingdom
Duration: Jul 11 2010Jul 14 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6172 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other1st International Conference on Interactive Theorem Proving, ITP 2010
Country/TerritoryUnited Kingdom


  • optimizing compilers
  • program transformations
  • temporal logic
  • theorem proving

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'A framework for formal verification of compiler optimizations'. Together they form a unique fingerprint.

Cite this