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 metadatas

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/hal-01096110
Contributor : Christophe Alias <>
Submitted on : Tuesday, December 16, 2014 - 5:42:38 PM
Last modification on : Thursday, November 21, 2019 - 2:41:11 AM
Long-term archiving on: Monday, March 23, 2015 - 2:28:43 PM

File

sas2014.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01096110, version 1

Collections

Citation

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

Share

Metrics

Record views

272

Files downloads

238