An Abstract Domain to Infer Octagonal Constraints with Absolute Value

Abstract : The octagon abstract domain, devoted to discovering octagonal constraints (also called Unit Two Variable Per Inequality or UTVPI constraints) of a program, is one of the most commonly used numerical abstractions in practice, due to its quadratic memory complexity and cubic time complexity. However, the octagon domain itself is restricted to express convex sets and has limitations in handling non-convex properties which are sometimes required for proving some numerical properties in a program. In this paper, we intend to extend the octagon abstract domain with absolute value, to infer certain non-convex properties by exploiting the absolute value function. More precisely, the new domain can infer relations of the form {±X ± Y ≤ c, ±X ± |Y| ≤ d, ±|X| ± |Y| ≤ e}. We provide algorithms for domain operations such that the new domain still enjoys the same asymptotic complexity as the octagon domain. Moreover, we present an approach to support strict inequalities over rational or real-valued variables in this domain, which also fits for the octagon domain. Experimental results of our prototype are encouraging; The new domain is scalable and able to find non-convex invariants of interest in practice but without too much overhead (compared with that using octagons).
Type de document :
Communication dans un congrès
21st International Static Analysis Symposium (SAS'14), Sep 2014, Munich, Germany. Springer, 8373, pp.18, 2014, Lecture Note in Computer Science. 〈http://cs.uni-muenster.de/sev/sas14/〉. 〈10.1007/978-3-319-10936-7_7〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01105217
Contributeur : Antoine Miné <>
Soumis le : mardi 20 janvier 2015 - 15:31:03
Dernière modification le : vendredi 25 mai 2018 - 12:02:07
Document(s) archivé(s) le : mardi 21 avril 2015 - 10:11:16

Fichier

article-chen-al-sas14.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Liqian Chen, Jiangchao Liu, Antoine Miné, Deepak Kapur, Ji Wang. An Abstract Domain to Infer Octagonal Constraints with Absolute Value. 21st International Static Analysis Symposium (SAS'14), Sep 2014, Munich, Germany. Springer, 8373, pp.18, 2014, Lecture Note in Computer Science. 〈http://cs.uni-muenster.de/sev/sas14/〉. 〈10.1007/978-3-319-10936-7_7〉. 〈hal-01105217〉

Partager

Métriques

Consultations de la notice

300

Téléchargements de fichiers

124