Linear absolute value relation analysis

Liqian Chen; Antoine Miné; Ji Wang; Patrick Cousot

doi:10.1007/978-3-642-19718-5_9

Linear absolute value relation analysis

Liqian Chen, Antoine Miné, Ji Wang, Patrick Cousot

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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 (∑ _k a _k x _k + ∑ _k b _k |x _k | ≤ c), 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.

Original language	English (US)
Title of host publication	Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Proceedings
Pages	156-175
Number of pages	20
DOIs	https://doi.org/10.1007/978-3-642-19718-5_9
State	Published - 2011
Event	20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011 - Saarbrucken, Germany Duration: Mar 26 2011 → Apr 3 2011

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	6602 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011
Country/Territory	Germany
City	Saarbrucken
Period	3/26/11 → 4/3/11

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-642-19718-5_9

Cite this

Chen, L., Miné, A., Wang, J., & Cousot, P. (2011). Linear absolute value relation analysis. In Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Proceedings (pp. 156-175). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6602 LNCS). https://doi.org/10.1007/978-3-642-19718-5_9

Linear absolute value relation analysis. / Chen, Liqian; Miné, Antoine; Wang, Ji et al.
Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Proceedings. 2011. p. 156-175 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6602 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Chen, L, Miné, A, Wang, J & Cousot, P 2011, Linear absolute value relation analysis. in Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6602 LNCS, pp. 156-175, 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrucken, Germany, 3/26/11. https://doi.org/10.1007/978-3-642-19718-5_9

Chen L, Miné A, Wang J, Cousot P. Linear absolute value relation analysis. In Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Proceedings. 2011. p. 156-175. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-19718-5_9

Chen, Liqian ; Miné, Antoine ; Wang, Ji et al. / Linear absolute value relation analysis. Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Proceedings. 2011. pp. 156-175 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{cc19981515094422ad61818c5d350e04,

title = "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 (∑ k a k x k + ∑ k b k |x k | ≤ c), 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.",

author = "Liqian Chen and Antoine Min{\'e} and Ji Wang and Patrick Cousot",

note = "Copyright: Copyright 2011 Elsevier B.V., All rights reserved.; 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011 ; Conference date: 26-03-2011 Through 03-04-2011",

year = "2011",

doi = "10.1007/978-3-642-19718-5_9",

language = "English (US)",

isbn = "9783642197178",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "156--175",

booktitle = "Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Proceedings",

}

TY - GEN

T1 - Linear absolute value relation analysis

AU - Chen, Liqian

AU - Miné, Antoine

AU - Wang, Ji

AU - Cousot, Patrick

PY - 2011

Y1 - 2011

N2 - 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 (∑ k a k x k + ∑ k b k |x k | ≤ c), 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.

AB - 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 (∑ k a k x k + ∑ k b k |x k | ≤ c), 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.

UR - http://www.scopus.com/inward/record.url?scp=79953232742&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=79953232742&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-19718-5_9

DO - 10.1007/978-3-642-19718-5_9

M3 - Conference contribution

AN - SCOPUS:79953232742

SN - 9783642197178

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 156

EP - 175

BT - Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Proceedings

T2 - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011

Y2 - 26 March 2011 through 3 April 2011

ER -

Linear absolute value relation analysis

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this