TVOC: A translation validator for optimizing compilers

Clark Barrett; Yi Fang; Benjamin Goldberg; Ying Hu; Amir Pnueli; Lenore Zuck

doi:10.1007/11513988_29

TVOC: A translation validator for optimizing compilers

Clark Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, Lenore Zuck

Research output: Contribution to journal › Conference article › peer-review

Abstract

We describe a tool called TVOC, that uses the translation validation approach to check the validity of compiler optimizations: for a given source program, TVOC proves the equivalence of the source code and the target code produced by running the compiler. There are two phases to the verification process: the first phase verifies loop transformations using the proof rule PERMUTE; the second phase verifies structure-preserving optimizations using the proof rule VALIDATE. Verification conditions are validated using the automatic theorem prover CVC Lite.

Original language	English (US)
Pages (from-to)	291-295
Number of pages	5
Journal	Lecture Notes in Computer Science
Volume	3576
DOIs	https://doi.org/10.1007/11513988_29
State	Published - 2005
Event	17th International Conference on Computer Aided Verification, CAV 2005 - Edinburgh, Scotland, United Kingdom Duration: Jul 6 2005 → Jul 10 2005

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/11513988_29

Cite this

@article{1fd843a1e1f54f95807a5425a89089d2,

title = "TVOC: A translation validator for optimizing compilers",

abstract = "We describe a tool called TVOC, that uses the translation validation approach to check the validity of compiler optimizations: for a given source program, TVOC proves the equivalence of the source code and the target code produced by running the compiler. There are two phases to the verification process: the first phase verifies loop transformations using the proof rule PERMUTE; the second phase verifies structure-preserving optimizations using the proof rule VALIDATE. Verification conditions are validated using the automatic theorem prover CVC Lite.",

author = "Clark Barrett and Yi Fang and Benjamin Goldberg and Ying Hu and Amir Pnueli and Lenore Zuck",

year = "2005",

doi = "10.1007/11513988_29",

language = "English (US)",

volume = "3576",

pages = "291--295",

journal = "Lecture Notes in Computer Science",

issn = "0302-9743",

publisher = "Springer Science and Business Media Deutschland GmbH",

note = "17th International Conference on Computer Aided Verification, CAV 2005 ; Conference date: 06-07-2005 Through 10-07-2005",

}

TY - JOUR

T1 - TVOC

T2 - 17th International Conference on Computer Aided Verification, CAV 2005

AU - Barrett, Clark

AU - Fang, Yi

AU - Goldberg, Benjamin

AU - Hu, Ying

AU - Pnueli, Amir

AU - Zuck, Lenore

PY - 2005

Y1 - 2005

N2 - We describe a tool called TVOC, that uses the translation validation approach to check the validity of compiler optimizations: for a given source program, TVOC proves the equivalence of the source code and the target code produced by running the compiler. There are two phases to the verification process: the first phase verifies loop transformations using the proof rule PERMUTE; the second phase verifies structure-preserving optimizations using the proof rule VALIDATE. Verification conditions are validated using the automatic theorem prover CVC Lite.

AB - We describe a tool called TVOC, that uses the translation validation approach to check the validity of compiler optimizations: for a given source program, TVOC proves the equivalence of the source code and the target code produced by running the compiler. There are two phases to the verification process: the first phase verifies loop transformations using the proof rule PERMUTE; the second phase verifies structure-preserving optimizations using the proof rule VALIDATE. Verification conditions are validated using the automatic theorem prover CVC Lite.

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

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

U2 - 10.1007/11513988_29

DO - 10.1007/11513988_29

M3 - Conference article

AN - SCOPUS:26444608451

SN - 0302-9743

VL - 3576

SP - 291

EP - 295

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

Y2 - 6 July 2005 through 10 July 2005

ER -

TVOC: A translation validator for optimizing compilers

Abstract

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this