Improved Invariant Generation for Tvoc

Yi Fang, Lenore D. Zuck

Research output: Contribution to journalArticlepeer-review

Abstract

The NYU Tvoc project applies the method of translation validation to verify that optimized code is semantically equivalent to the unoptimized code, by establishing, for each run of the optimizing compiler, a set of verification conditions (VCs) whose validity implies the correctness of the optimized run. The core of Tvoc is Tvoc-sp, that handles structure preserving optimizations, i.e., optimizations that do not alter the inner loop structures. The underlying proof rule, Val, on whose soundness Tvoc-sp is based, requires, among other things, to generating invariants at each "cutpoint" of the control graph of both source and target codes. The current implementation of Tvoc-sp employs somewhat naïve fix-point computations to obtain the invariants. In this paper, we propose an alternative method to compute invartiants which is based on simple data-flow analysis techniques.

Original languageEnglish (US)
Pages (from-to)21-35
Number of pages15
JournalElectronic Notes in Theoretical Computer Science
Volume176
Issue number3 SPEC. ISS.
DOIs
StatePublished - Jul 19 2007

Keywords

  • Translation validation
  • data abstraction
  • data-flow analysis
  • invariant generation

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Improved Invariant Generation for Tvoc'. Together they form a unique fingerprint.

Cite this