A framework for formal verification of compiler optimizations

William Mansky; Elsa Gunter

doi:10.1007/978-3-642-14052-5_26

A framework for formal verification of compiler optimizations

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Interactive Theorem Proving - First International Conference, ITP 2010, Proceedings
Pages	371-386
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-642-14052-5_26
State	Published - 2010
Event	1st International Conference on Interactive Theorem Proving, ITP 2010 - Edinburgh, United Kingdom Duration: Jul 11 2010 → Jul 14 2010

Publication series

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

Other

Other	1st International Conference on Interactive Theorem Proving, ITP 2010
Country/Territory	United Kingdom
City	Edinburgh
Period	7/11/10 → 7/14/10

Keywords

optimizing compilers
program transformations
temporal logic
theorem proving

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Online availability

10.1007/978-3-642-14052-5_26

Library availability

Discover UIUC Full Text

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

A framework for formal verification of compiler optimizations. / Mansky, William; Gunter, Elsa.
Interactive Theorem Proving - First International Conference, ITP 2010, Proceedings. 2010. p. 371-386 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6172 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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

@inproceedings{b2931a8f27cc49b78fae6b9cfa5e21f9,

title = "A framework for formal verification of compiler optimizations",

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.",

keywords = "optimizing compilers, program transformations, temporal logic, theorem proving",

author = "William Mansky and Elsa Gunter",

year = "2010",

doi = "10.1007/978-3-642-14052-5_26",

language = "English (US)",

isbn = "3642140513",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "371--386",

booktitle = "Interactive Theorem Proving - First International Conference, ITP 2010, Proceedings",

note = "1st International Conference on Interactive Theorem Proving, ITP 2010 ; Conference date: 11-07-2010 Through 14-07-2010",

}

TY - GEN

T1 - A framework for formal verification of compiler optimizations

AU - Mansky, William

AU - Gunter, Elsa

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

KW - optimizing compilers

KW - program transformations

KW - temporal logic

KW - theorem proving

UR - http://www.scopus.com/inward/record.url?scp=77955241845&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=77955241845&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-14052-5_26

DO - 10.1007/978-3-642-14052-5_26

M3 - Conference contribution

AN - SCOPUS:77955241845

SN - 3642140513

SN - 9783642140518

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 371

EP - 386

BT - Interactive Theorem Proving - First International Conference, ITP 2010, Proceedings

T2 - 1st International Conference on Interactive Theorem Proving, ITP 2010

Y2 - 11 July 2010 through 14 July 2010

ER -

A framework for formal verification of compiler optimizations

Abstract

Publication series

Other

Keywords

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this