TVOC: A translation validator for optimizing compilers

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

Research output: Contribution to journalConference articlepeer-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 languageEnglish (US)
Pages (from-to)291-295
Number of pages5
JournalLecture Notes in Computer Science
Volume3576
DOIs
StatePublished - 2005
Event17th International Conference on Computer Aided Verification, CAV 2005 - Edinburgh, Scotland, United Kingdom
Duration: Jul 6 2005Jul 10 2005

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'TVOC: A translation validator for optimizing compilers'. Together they form a unique fingerprint.

Cite this