A framework for formal verification of compiler optimizations

William Mansky, Elsa Gunter

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

Abstract

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
Pages371-386
Number of pages16
DOIs
StatePublished - Aug 10 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

Other

Other1st International Conference on Interactive Theorem Proving, ITP 2010
CountryUnited Kingdom
CityEdinburgh
Period7/11/107/14/10

Keywords

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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

  • Cite this

    Mansky, W., & Gunter, E. (2010). A framework for formal verification of compiler optimizations. In Interactive Theorem Proving - First International Conference, ITP 2010, Proceedings (pp. 371-386). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6172 LNCS). https://doi.org/10.1007/978-3-642-14052-5_26