Linear Absolute Value Relation Analysis

Abstract : Linear relation analysis (polyhedral analysis), devoted to discovering linear invariant relations among variables of a program, remains one of the most powerful abstract interpretations but is subject to convexity limitations. Absolute value enjoys piecewise linear expressiveness and thus natively fits to encode certain non-convex properties. Based on this insight, we propose to use linear absolute value relation analysis to discover linear relations among values and absolute values of program variables. Under the framework of abstract interpretation, the analysis yields a new numerical abstract domain, namely the abstract domain of linear absolute value inequalities, which can be used to analyze programs involving piecewise linear behaviors (e.g., due to conditional branches or absolute value function calls). Experimental results of our prototype are encouraging; The new abstract domain can find non-convex invariants of interest in practice.
Type de document :
Communication dans un congrès
Gilles Barthe. ESOP 2011 : 20th European Symposium on Programming, Mar 2011, Saarbrücken, Germany. Springer, 6602, pp.156-175, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-19718-5〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00648039
Contributeur : Antoine Miné <>
Soumis le : dimanche 4 décembre 2011 - 23:26:18
Dernière modification le : vendredi 25 mai 2018 - 12:02:05

Identifiants

Collections

Citation

Liqian Chen, Patrick Cousot, Antoine Miné, Ji Wang. Linear Absolute Value Relation Analysis. Gilles Barthe. ESOP 2011 : 20th European Symposium on Programming, Mar 2011, Saarbrücken, Germany. Springer, 6602, pp.156-175, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-19718-5〉. 〈hal-00648039〉

Partager

Métriques

Consultations de la notice

293