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