An abstract domain of uninterpreted functions

Graeme Gange; Jorge A. Navas; Peter Schachte; Harald Søndergaard; Peter J. Stuckey

doi:10.1007/978-3-662-49122-5_4

An abstract domain of uninterpreted functions

Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

13 Citations (Scopus)

Abstract

We revisit relational static analysis of numeric variables. Such analyses face two difficulties. First, even inexpensive relational domains scale too poorly to be practical for large code-bases. Second, to remain tractable they have extremely coarse handling of non-linear relations. In this paper, we introduce the subterm domain, a weakly relational abstract domain for inferring equivalences amongst sub- expressions, based on the theory of uninterpreted functions. This pro- vides an extremely cheap approach for enriching non-relational domains with relational information, and enhances precision of both relational and non-relational domains in the presence of non-linear operations. We evaluate the idea in the context of the software verification tool Sea Horn.

Original language	English
Title of host publication	Verification, Model Checking, and Abstract Interpretation
Subtitle of host publication	17th International Conference, VMCAI 2016 St. Petersburg, FL, USA, January 17–19, 2016 Proceedings
Editors	Barbara Jobstmann, K. Rustan M. Leino
Place of Publication	Berlin Germany
Publisher	Springer
Pages	85-103
Number of pages	19
ISBN (Electronic)	9783662491225
ISBN (Print)	9783662491218
DOIs	https://doi.org/10.1007/978-3-662-49122-5_4
Publication status	Published - 2016
Externally published	Yes
Event	Verification, Model Checking and Abstract Interpretation 2016 - St. Petersburg, United States of America Duration: 17 Jan 2016 → 19 Jan 2016 Conference number: 17th https://conf.researchr.org/home/VMCAI-2016

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	9583
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	Verification, Model Checking and Abstract Interpretation 2016
Abbreviated title	VMCAI 2016
Country/Territory	United States of America
City	St. Petersburg
Period	17/01/16 → 19/01/16
Internet address	https://conf.researchr.org/home/VMCAI-2016

Access to Document

10.1007/978-3-662-49122-5_4

Cite this

Gange, G., Navas, J. A., Schachte, P., Søndergaard, H., & Stuckey, P. J. (2016). An abstract domain of uninterpreted functions. In B. Jobstmann, & K. R. M. Leino (Eds.), Verification, Model Checking, and Abstract Interpretation: 17th International Conference, VMCAI 2016 St. Petersburg, FL, USA, January 17–19, 2016 Proceedings (pp. 85-103). (Lecture Notes in Computer Science ; Vol. 9583). Springer. https://doi.org/10.1007/978-3-662-49122-5_4

Gange, Graeme ; Navas, Jorge A. ; Schachte, Peter et al. / An abstract domain of uninterpreted functions. Verification, Model Checking, and Abstract Interpretation: 17th International Conference, VMCAI 2016 St. Petersburg, FL, USA, January 17–19, 2016 Proceedings. editor / Barbara Jobstmann ; K. Rustan M. Leino. Berlin Germany : Springer, 2016. pp. 85-103 (Lecture Notes in Computer Science ).

@inproceedings{3ee68b11c1b74d83b524bc274fb7864b,

title = "An abstract domain of uninterpreted functions",

abstract = "We revisit relational static analysis of numeric variables. Such analyses face two difficulties. First, even inexpensive relational domains scale too poorly to be practical for large code-bases. Second, to remain tractable they have extremely coarse handling of non-linear relations. In this paper, we introduce the subterm domain, a weakly relational abstract domain for inferring equivalences amongst sub- expressions, based on the theory of uninterpreted functions. This pro- vides an extremely cheap approach for enriching non-relational domains with relational information, and enhances precision of both relational and non-relational domains in the presence of non-linear operations. We evaluate the idea in the context of the software verification tool Sea Horn.",

author = "Graeme Gange and Navas, {Jorge A.} and Peter Schachte and Harald S{\o}ndergaard and Stuckey, {Peter J.}",

year = "2016",

doi = "10.1007/978-3-662-49122-5_4",

language = "English",

isbn = "9783662491218",

series = "Lecture Notes in Computer Science ",

publisher = "Springer",

pages = "85--103",

editor = "Barbara Jobstmann and {M. Leino}, {K. Rustan }",

booktitle = "Verification, Model Checking, and Abstract Interpretation",

note = "Verification, Model Checking and Abstract Interpretation 2016, VMCAI 2016 ; Conference date: 17-01-2016 Through 19-01-2016",

url = "https://conf.researchr.org/home/VMCAI-2016",

}

Gange, G, Navas, JA, Schachte, P, Søndergaard, H & Stuckey, PJ 2016, An abstract domain of uninterpreted functions. in B Jobstmann & KR M. Leino (eds), Verification, Model Checking, and Abstract Interpretation: 17th International Conference, VMCAI 2016 St. Petersburg, FL, USA, January 17–19, 2016 Proceedings. Lecture Notes in Computer Science , vol. 9583, Springer, Berlin Germany, pp. 85-103, Verification, Model Checking and Abstract Interpretation 2016, St. Petersburg, Florida, United States of America, 17/01/16. https://doi.org/10.1007/978-3-662-49122-5_4

An abstract domain of uninterpreted functions. / Gange, Graeme; Navas, Jorge A.; Schachte, Peter et al.
Verification, Model Checking, and Abstract Interpretation: 17th International Conference, VMCAI 2016 St. Petersburg, FL, USA, January 17–19, 2016 Proceedings. ed. / Barbara Jobstmann; K. Rustan M. Leino. Berlin Germany: Springer, 2016. p. 85-103 (Lecture Notes in Computer Science ; Vol. 9583).

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

TY - GEN

T1 - An abstract domain of uninterpreted functions

AU - Gange, Graeme

AU - Navas, Jorge A.

AU - Schachte, Peter

AU - Søndergaard, Harald

AU - Stuckey, Peter J.

N1 - Conference code: 17th

PY - 2016

Y1 - 2016

N2 - We revisit relational static analysis of numeric variables. Such analyses face two difficulties. First, even inexpensive relational domains scale too poorly to be practical for large code-bases. Second, to remain tractable they have extremely coarse handling of non-linear relations. In this paper, we introduce the subterm domain, a weakly relational abstract domain for inferring equivalences amongst sub- expressions, based on the theory of uninterpreted functions. This pro- vides an extremely cheap approach for enriching non-relational domains with relational information, and enhances precision of both relational and non-relational domains in the presence of non-linear operations. We evaluate the idea in the context of the software verification tool Sea Horn.

AB - We revisit relational static analysis of numeric variables. Such analyses face two difficulties. First, even inexpensive relational domains scale too poorly to be practical for large code-bases. Second, to remain tractable they have extremely coarse handling of non-linear relations. In this paper, we introduce the subterm domain, a weakly relational abstract domain for inferring equivalences amongst sub- expressions, based on the theory of uninterpreted functions. This pro- vides an extremely cheap approach for enriching non-relational domains with relational information, and enhances precision of both relational and non-relational domains in the presence of non-linear operations. We evaluate the idea in the context of the software verification tool Sea Horn.

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

U2 - 10.1007/978-3-662-49122-5_4

DO - 10.1007/978-3-662-49122-5_4

M3 - Conference Paper

AN - SCOPUS:84955327158

SN - 9783662491218

T3 - Lecture Notes in Computer Science

SP - 85

EP - 103

BT - Verification, Model Checking, and Abstract Interpretation

A2 - Jobstmann, Barbara

A2 - M. Leino, K. Rustan

PB - Springer

CY - Berlin Germany

T2 - Verification, Model Checking and Abstract Interpretation 2016

Y2 - 17 January 2016 through 19 January 2016

ER -

Gange G, Navas JA, Schachte P, Søndergaard H, Stuckey PJ. An abstract domain of uninterpreted functions. In Jobstmann B, M. Leino KR, editors, Verification, Model Checking, and Abstract Interpretation: 17th International Conference, VMCAI 2016 St. Petersburg, FL, USA, January 17–19, 2016 Proceedings. Berlin Germany: Springer. 2016. p. 85-103. (Lecture Notes in Computer Science ). doi: 10.1007/978-3-662-49122-5_4

An abstract domain of uninterpreted functions

Abstract

Publication series

Conference

Access to Document

Other files and links

Cite this