Translation and run-time validation of optimized code

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

Research output: Contribution to journalConference articlepeer-review


The translation and run-time validation approaches of optimizing compilers are discussed. The translation validation approach performs a validation check after every run of the compiler, producing a formal proof that the target code is a correct implementation of the source code. A set of permutation rules is also described for more aggressive optimizations which, typically, alter the loop structure of the code, such as loop distribution and fusion, loop tiling, and lop interchanges. The run-time validation approach of speculative loop optimizations, that involves run-time tests, ensures the correctness of loop optimizations which neither the compiler nor compiler-validation techniques can guarantee the correctness.

Original languageEnglish (US)
Pages (from-to)179-200
Number of pages22
JournalElectronic Notes in Theoretical Computer Science
Issue number4
StatePublished - Dec 2002
EventRV'02, Runtime Verification 2002 (FLoC satellite Event) - Copenhagen, Denmark
Duration: Jul 26 2002Jul 26 2002

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Translation and run-time validation of optimized code'. Together they form a unique fingerprint.

Cite this