Abstract Interpretation over Non-Lattice Abstract Domains. Gange, G., Navas, J. A., Schachte, P., Søndergaard, H., & Stuckey, P. J. In Logozzo, F. & Fähndrich, M., editors, Static Analysis, volume 7935, of Lecture Notes in Computer Science, pages 6–24, 2013. Springer. doi abstract bibtex 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.
@InProceedings{Gan-Nav-Sch-Son-Stu_SAS13,
author = {Graeme Gange and
Jorge A. Navas and
Peter Schachte and
Harald S{\o}ndergaard and
Peter J. Stuckey},
title = {Abstract Interpretation over Non-Lattice Abstract Domains},
editor = {F. Logozzo and M. F{\"a}hndrich},
booktitle = {Static Analysis},
series = {Lecture Notes in Computer Science},
volume = {7935},
pages = {6--24},
publisher = {Springer},
year = {2013},
doi = {10.1007/978-3-642-38856-9_3},
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.},
keywords = {Fixed points, Abstract domains, Lattice theory},
}
Downloads: 0
{"_id":"n4a35djMmtZP2Jqm6","bibbaseid":"gange-navas-schachte-sndergaard-stuckey-abstractinterpretationovernonlatticeabstractdomains-2013","author_short":["Gange, G.","Navas, J. A.","Schachte, P.","Søndergaard, H.","Stuckey, P. J."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Graeme"],"propositions":[],"lastnames":["Gange"],"suffixes":[]},{"firstnames":["Jorge","A."],"propositions":[],"lastnames":["Navas"],"suffixes":[]},{"firstnames":["Peter"],"propositions":[],"lastnames":["Schachte"],"suffixes":[]},{"firstnames":["Harald"],"propositions":[],"lastnames":["Søndergaard"],"suffixes":[]},{"firstnames":["Peter","J."],"propositions":[],"lastnames":["Stuckey"],"suffixes":[]}],"title":"Abstract Interpretation over Non-Lattice Abstract Domains","editor":[{"firstnames":["F."],"propositions":[],"lastnames":["Logozzo"],"suffixes":[]},{"firstnames":["M."],"propositions":[],"lastnames":["Fähndrich"],"suffixes":[]}],"booktitle":"Static Analysis","series":"Lecture Notes in Computer Science","volume":"7935","pages":"6–24","publisher":"Springer","year":"2013","doi":"10.1007/978-3-642-38856-9_3","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.","keywords":"Fixed points, Abstract domains, Lattice theory","bibtex":"@InProceedings{Gan-Nav-Sch-Son-Stu_SAS13,\n author = {Graeme Gange and \n\t\tJorge A. Navas and \n\t\tPeter Schachte and\n\t\tHarald S{\\o}ndergaard and \n\t\tPeter J. Stuckey},\n title = {Abstract Interpretation over Non-Lattice Abstract Domains},\n editor = {F. Logozzo and M. F{\\\"a}hndrich},\n booktitle = {Static Analysis},\n series = {Lecture Notes in Computer Science},\n volume = {7935},\n pages = {6--24},\n publisher = {Springer},\n year = {2013},\n doi = {10.1007/978-3-642-38856-9_3},\n abstract = {The classical theoretical framework for static analysis of\n\t\tprograms is abstract interpretation. Much of the power and \n\t\telegance of that framework rests on the assumption that an \n\t\tabstract domain is a lattice. Nonetheless, and for good reason,\n\t\tthe literature on program analysis provides many examples of \n\t\tnon-lattice domains, including non-convex numeric domains. \n\t\tThe lack of domain structure, however, has negative \n\t\tconsequences, both for the precision of program analysis and \n\t\tfor the termination of standard Kleene iteration. In this paper \n\t\twe explore these consequences and present general remedies.},\n keywords = {Fixed points, Abstract domains, Lattice theory},\n}\n\n","author_short":["Gange, G.","Navas, J. A.","Schachte, P.","Søndergaard, H.","Stuckey, P. J."],"editor_short":["Logozzo, F.","Fähndrich, M."],"key":"Gan-Nav-Sch-Son-Stu_SAS13","id":"Gan-Nav-Sch-Son-Stu_SAS13","bibbaseid":"gange-navas-schachte-sndergaard-stuckey-abstractinterpretationovernonlatticeabstractdomains-2013","role":"author","urls":{},"keyword":["Fixed points","Abstract domains","Lattice theory"],"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"people.eng.unimelb.edu.au/harald/bibbase.bib","dataSources":["yWvm3kzg5vKQAPLm7","ofmsZryxNDBSpE7j5","9aC4cxLD8D6oJ3FLN","wpkuJrZJJtqra3FbL","XqcrNTrCCBr9mSd37"],"keywords":["fixed points","abstract domains","lattice theory"],"search_terms":["abstract","interpretation","over","non","lattice","abstract","domains","gange","navas","schachte","søndergaard","stuckey"],"title":"Abstract Interpretation over Non-Lattice Abstract Domains","year":2013}