Improved Invariant Generation for TVOC

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 naive 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.