Transitive Closures of Affine Integer Tuple Relations and their Overapproximations

Sven Verdoolaege 1 Albert Cohen 1 Anna Beletska 2
1 Parkas - Parallélisme de Kahn Synchrone
DI-ENS - Département d'informatique de l'École normale supérieure, ENS Paris - École normale supérieure - Paris, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
2 ALCHEMY - Architectures, Languages and Compilers to Harness the End of Moore Years
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : The set of paths in a graph is an important concept with many applications in system analysis. In the context of integer tuple relations, which can be used to represent possibly infinite graphs, this set corresponds to the transitive closure of the relation representing the graph. Relations described using only affine constraints and projection are fairly efficient to use in practice and capture Presburger arithmetic. Unfortunately, the transitive closure of such a quasi-affine relation may not be quasi-affine and so there is a need for approximations. In particular, most applications in system analysis require overapproximations. Previous work has mostly focused either on underapproximations or special cases of affine relations. We present a novel algorithm for computing overapproximations of transitive closures for the general case of quasi-affine relations (convex or not). Experiments on non-trivial relations from real-world applications show our algorithm to be on average more accurate and faster than the best known alternatives.
Type de document :
Communication dans un congrès
Eran Yahav. SAS 2011 - The 18th International Static Analysis Symposium, Sep 2011, Venice, Italy. Springer, 6887, pp.216-232, 2011, LNCS. 〈10.1007/978-3-642-23702-7_18〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00645221
Contributeur : Albert Cohen <>
Soumis le : mardi 29 novembre 2011 - 11:48:36
Dernière modification le : jeudi 9 février 2017 - 15:54:01
Document(s) archivé(s) le : lundi 5 décembre 2016 - 08:59:37

Fichier

sas.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Sven Verdoolaege, Albert Cohen, Anna Beletska. Transitive Closures of Affine Integer Tuple Relations and their Overapproximations. Eran Yahav. SAS 2011 - The 18th International Static Analysis Symposium, Sep 2011, Venice, Italy. Springer, 6887, pp.216-232, 2011, LNCS. 〈10.1007/978-3-642-23702-7_18〉. 〈hal-00645221〉

Partager

Métriques

Consultations de
la notice

809

Téléchargements du document

178