Skip to Main content Skip to Navigation
New interface
Conference papers

On Program Equivalence with Reductions

Abstract : Program equivalence is a well-known problem with a wide range of applications, such as algorithm recognition, program verification and program optimization. This problem is also known to be undecidable if the class of programs is rich enough, in which case semi-algorithms are commonly used. We focus on programs represented as Systems of Affine Recurrence Equations (SARE), defined over parametric polyhedral domains, a well known formalism for the polyhedral model. SAREs include as a proper subset, the class of affine control loop programs. Several program equivalence semi-algorithms were already proposed for this class. Some take into account algebraic properties such as associativity and commutativity. To the best of our knowledge, none of them manage reductions, i.e., accumulations of a parametric number of sub-expressions using an associative and commutative operator. Our main contribution is a new semi-algorithm to manage reductions. In particular, we outline the ties between this problem and the perfect matching problem in a parametric bipartite graph.
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download
Contributor : Christophe Alias Connect in order to contact the contributor
Submitted on : Tuesday, December 16, 2014 - 5:42:38 PM
Last modification on : Friday, November 18, 2022 - 9:24:15 AM
Long-term archiving on: : Monday, March 23, 2015 - 2:28:43 PM


Files produced by the author(s)


  • HAL Id : hal-01096110, version 1



Guillaume Iooss, Christophe Alias, Sanjay Rajopadhye. On Program Equivalence with Reductions. 21st International Static Analysis Symposium (SAS'14), Sep 2014, Munich, Germany. ⟨hal-01096110⟩



Record views


Files downloads