c © Springer Accepted for CAV 2009 Equivalence Checking of Static Affine Programs using Widening to Handle Recurrences

Abstract. 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 functionality, however, and this paper presents an automatic method for constructing equivalence proofs for the class of static affine programs. The equiva-lence checking is performed on a dependence graph abstraction and uses a new approach based on widening to handle recurrences. Unlike tran-sitive closure based approaches, this widening approach can also handle non-uniform recurrences. The implementation is publicly available and is the first of its kind to fully support commutative operations.