Linear Absolute Value Relation Analysis - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2011

Linear Absolute Value Relation Analysis

Résumé

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.

Dates et versions

hal-00648039 , version 1 (04-12-2011)

Identifiants

Citer

Liqian Chen, Patrick Cousot, Antoine Miné, Ji Wang. Linear Absolute Value Relation Analysis. ESOP 2011 : 20th European Symposium on Programming, Mar 2011, Saarbrücken, Germany. pp.156-175, ⟨10.1007/978-3-642-19718-5⟩. ⟨hal-00648039⟩
176 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More