Title: Equivalence checking of static affine programs using widening to handle recurrences
Authors: Verdoolaege, Sven ×
Janssens, Gerda
Bruynooghe, Maurice #
Issue Date: Oct-2012
Publisher: Association for Computing Machinery
Series Title: ACM Transactions on Programming Languages and Systems vol:34 issue:3 pages:11:1-11:35
Article number: 11
Abstract: 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.
ISSN: 0164-0925
Publication status: published
KU Leuven publication type: IT
Appears in Collections:Informatics Section
× corresponding author
# (joint) last author

Files in This Item:
File Description Status SizeFormat
toplas.pdfArticle Published 521KbAdobe PDFView/Open


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

© Web of science