Equivalence Checking of Static Affine Programs using Widening to Handle Recurrences

Designers often apply manual or semi-automatic loop and data transformations on array and loop intensive programs to improve performance. The transformations should preserve the function-ality, however, and this paper presents an automatic method to proof equivalence for the class of static affine programs. The equivalence checking is performed on a dependence graph abstraction and uses a new approach based onwidening to handle recurrences. In contrast to transitive closure based approaches, this widening approach does not require uniform recurrences. The implemen-tation is publicly available and is the first of its kind to fully support commutative operations