Title: Equivalence checking of static affine programs using widening to handle recurrences
Authors: Verdoolaege, Sven
Janssens, Gerda
Bruynooghe, Maurice
Issue Date: Sep-2009
Publisher: Department of Computer Science, K.U.Leuven
Series Title: CW Reports vol:CW565
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 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.
Publication status: published
KU Leuven publication type: IR
Appears in Collections:Informatics Section

Files in This Item:
File Description Status SizeFormat
CW565.pdfDocument Published 433KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.