Linear absolute value relation analysis

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

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish (US)
Title of host publicationProgramming 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
Pages156-175
Number of pages20
DOIs
StatePublished - 2011
Event20th 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 2011Apr 3 2011

Publication series

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

Other

Other20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011
CountryGermany
CitySaarbrucken
Period3/26/114/3/11

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Linear absolute value relation analysis'. Together they form a unique fingerprint.

  • 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