Validating more loop optimizations

Ying Hu, Clark Barrett, Benjamin Goldberg, Amir Pnueli

Research output: Contribution to journalConference articlepeer-review


Translation validation is a technique for ensuring that a translator, such as a compiler, produces correct results. Because complete verification of the translator itself is often infeasible, translation validation advocates coupling the verification task with the translation task, so that each run of the translator produces verification conditions which, if valid, prove the correctness of the translation. In previous work, the translation validation approach was used to give a framework for proving the correctness of a variety of compiler optimizations, with a recent focus on loop transformations. However, some of these ideas were preliminary and had not been implemented. Additionally, there were examples of common loop transformations which could not be handled by our previous approaches. This paper addresses these issues. We introduce a new rule Reduce for loop reduction transformations, and we generalize our previous rule Validate so that it can handle more transformations involving loops. We then describe how all of this (including some previous theoretical work) is implemented in our compiler validation tool TVOC.

Original languageEnglish (US)
Pages (from-to)69-84
Number of pages16
JournalElectronic Notes in Theoretical Computer Science
Issue number2
StatePublished - Dec 7 2005
EventProceedings of the Fourth International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2005) -
Duration: Apr 3 2005Apr 3 2005


  • Formal methods
  • Loop optimizations
  • Translation validation

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Validating more loop optimizations'. Together they form a unique fingerprint.

Cite this