ACM Transactions on Programming Languages and Systems vol:34 issue:3 pages:11:1-11:35
Designers often apply manual or semi-automatic loop and data
transformations on array and loop intensive programs to improve
It is crucial that such transformations preserve the
functionality of the program.
This paper presents an automatic
method for constructing equivalence proofs for the class of static affine
programs. The equivalence checking is performed on a dependence
graph abstraction and uses a new approach based on widening to
find the proper induction hypotheses for reasoning about
recurrences. Unlike transitive 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.