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.
Type de document :
Communication dans un congrès
21st International Static Analysis Symposium (SAS'14), Sep 2014, Munich, Germany. 2014, 〈http://cs.uni-muenster.de/sev/sas14/〉
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

Contributeur : Christophe Alias <>
Soumis le : mardi 16 décembre 2014 - 17:42:38
Dernière modification le : jeudi 8 février 2018 - 11:09:28
Document(s) archivé(s) le : lundi 23 mars 2015 - 14:28:43


Fichiers produits par l'(les) auteur(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. 2014, 〈http://cs.uni-muenster.de/sev/sas14/〉. 〈hal-01096110〉



Consultations de la notice


Téléchargements de fichiers