Sciweavers

CAV
2009
Springer

Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences

14 years 2 months ago
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 functionality, however, and this paper presents an automatic method for constructing equivalence proofs for the class of static affine programs. The equivaecking is performed on a dependence graph abstraction and uses a new approach based on widening to handle 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.
Sven Verdoolaege, Gerda Janssens, Maurice Bruynoog
Added 12 Aug 2010
Updated 12 Aug 2010
Type Conference
Year 2009
Where CAV
Authors Sven Verdoolaege, Gerda Janssens, Maurice Bruynooghe
Comments (0)