Abstract interpretation over non-lattice abstract domains

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

doi:10.1007/978-3-642-38856-9_3

Abstract interpretation over non-lattice abstract domains

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

12 Citations (Scopus)

Abstract

The classical theoretical framework for static analysis of programs is abstract interpretation. Much of the power and elegance of that framework rests on the assumption that an abstract domain is a lattice. Nonetheless, and for good reason, the literature on program analysis provides many examples of non-lattice domains, including non-convex numeric domains. The lack of domain structure, however, has negative consequences, both for the precision of program analysis and for the termination of standard Kleene iteration. In this paper we explore these consequences and present general remedies.

Original language	English
Title of host publication	Static Analysis - 20th International Symposium, SAS 2013, Proceedings
Publisher	Springer
Pages	6-24
Number of pages	19
ISBN (Print)	9783642388552
DOIs	https://doi.org/10.1007/978-3-642-38856-9_3
Publication status	Published - 26 Sep 2013
Externally published	Yes
Event	20th International Static Analysis Symposium, SAS 2013 - Seattle, WA, United States of America Duration: 20 Jun 2013 → 22 Jun 2013

Publication series

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

Conference

Conference	20th International Static Analysis Symposium, SAS 2013
Country	United States of America
City	Seattle, WA
Period	20/06/13 → 22/06/13

Access to Document

10.1007/978-3-642-38856-9_3

Link to publication in Scopus

Cite this

Gange, G., Navas, J. A., Schachte, P., Søndergaard, H., & Stuckey, P. J. (2013). Abstract interpretation over non-lattice abstract domains. In Static Analysis - 20th International Symposium, SAS 2013, Proceedings (pp. 6-24). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7935 LNCS). Springer. https://doi.org/10.1007/978-3-642-38856-9_3

Gange, Graeme ; Navas, Jorge A. ; Schachte, Peter ; Søndergaard, Harald ; Stuckey, Peter J. / Abstract interpretation over non-lattice abstract domains. Static Analysis - 20th International Symposium, SAS 2013, Proceedings. Springer, 2013. pp. 6-24 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{1c2a11b1f7a74751881aeeeb11c80097,

title = "Abstract interpretation over non-lattice abstract domains",

abstract = "The classical theoretical framework for static analysis of programs is abstract interpretation. Much of the power and elegance of that framework rests on the assumption that an abstract domain is a lattice. Nonetheless, and for good reason, the literature on program analysis provides many examples of non-lattice domains, including non-convex numeric domains. The lack of domain structure, however, has negative consequences, both for the precision of program analysis and for the termination of standard Kleene iteration. In this paper we explore these consequences and present general remedies.",

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

year = "2013",

month = sep

day = "26",

doi = "10.1007/978-3-642-38856-9_3",

language = "English",

isbn = "9783642388552",

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

publisher = "Springer",

pages = "6--24",

booktitle = "Static Analysis - 20th International Symposium, SAS 2013, Proceedings",

note = "20th International Static Analysis Symposium, SAS 2013 ; Conference date: 20-06-2013 Through 22-06-2013",

}

Gange, G, Navas, JA, Schachte, P, Søndergaard, H & Stuckey, PJ 2013, Abstract interpretation over non-lattice abstract domains. in Static Analysis - 20th International Symposium, SAS 2013, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7935 LNCS, Springer, pp. 6-24, 20th International Static Analysis Symposium, SAS 2013, Seattle, WA, United States of America, 20/06/13. https://doi.org/10.1007/978-3-642-38856-9_3

Abstract interpretation over non-lattice abstract domains. / Gange, Graeme; Navas, Jorge A.; Schachte, Peter; Søndergaard, Harald; Stuckey, Peter J.

Static Analysis - 20th International Symposium, SAS 2013, Proceedings. Springer, 2013. p. 6-24 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7935 LNCS).

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

TY - GEN

T1 - Abstract interpretation over non-lattice abstract domains

AU - Gange, Graeme

AU - Navas, Jorge A.

AU - Schachte, Peter

AU - Søndergaard, Harald

AU - Stuckey, Peter J.

PY - 2013/9/26

Y1 - 2013/9/26

N2 - The classical theoretical framework for static analysis of programs is abstract interpretation. Much of the power and elegance of that framework rests on the assumption that an abstract domain is a lattice. Nonetheless, and for good reason, the literature on program analysis provides many examples of non-lattice domains, including non-convex numeric domains. The lack of domain structure, however, has negative consequences, both for the precision of program analysis and for the termination of standard Kleene iteration. In this paper we explore these consequences and present general remedies.

AB - The classical theoretical framework for static analysis of programs is abstract interpretation. Much of the power and elegance of that framework rests on the assumption that an abstract domain is a lattice. Nonetheless, and for good reason, the literature on program analysis provides many examples of non-lattice domains, including non-convex numeric domains. The lack of domain structure, however, has negative consequences, both for the precision of program analysis and for the termination of standard Kleene iteration. In this paper we explore these consequences and present general remedies.

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

U2 - 10.1007/978-3-642-38856-9_3

DO - 10.1007/978-3-642-38856-9_3

M3 - Conference Paper

AN - SCOPUS:84884488361

SN - 9783642388552

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

SP - 6

EP - 24

BT - Static Analysis - 20th International Symposium, SAS 2013, Proceedings

PB - Springer

T2 - 20th International Static Analysis Symposium, SAS 2013

Y2 - 20 June 2013 through 22 June 2013

ER -

Gange G, Navas JA, Schachte P, Søndergaard H, Stuckey PJ. Abstract interpretation over non-lattice abstract domains. In Static Analysis - 20th International Symposium, SAS 2013, Proceedings. Springer. 2013. p. 6-24. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-38856-9_3