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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the Fourth Annual Symposium on Principles of Programming Languages, pp. 238–252. ACM (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the Sixth Annual Symposium on Principles of Programming Languages, pp. 269–282. ACM (1979)
Cousot, P., Cousot, R.: Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol. 631, pp. 269–295. Springer, Heidelberg (1992)
Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: Proceedings of the 38th Annual Symposium on Principles of Programming Languages, pp. 105–118. ACM (2011)
Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University (1990)
Ghorbal, K., Ivančić, F., Balakrishnan, G., Maeda, N., Gupta, A.: Donut domains: Efficient non-convex domains for abstract interpretation. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 235–250. Springer, Heidelberg (2012)
Gopan, D., Reps, T., Sagiv, M.: A framework for numeric analysis of array operations. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 338–350. ACM (2005)
Gotlieb, A., Leconte, M., Marre, B.: Constraint solving on modular integers. In: Proceedings of the Ninth International Workshop on Constraint Modelling and Reformulation (September 2010)
Halbwachs, N., Péron, M.: Discovering properties about arrays in simple programs. SIGPLAN Notices 43, 339–348 (2008)
Knuth, D.E.: The Art of Computer Programming, 2nd edn., vol. 2. Addison-Wesley (1981)
Navas, J.A., Schachte, P., Søndergaard, H., Stuckey, P.J.: Signedness-agnostic program analysis: Precise integer bounds for low-level code. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 115–130. Springer, Heidelberg (2012)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer (1999)
Regehr, J., Duongsaa, U.: Deriving abstract transfer functions for analyzing embedded software. In: LCTES 2006: Proceedings of the 2006 ACM SIGPLAN/SIGBED Conference on Language, Compilers, and Tool Support for Embedded Systems, pp. 34–43. ACM (2006)
Sălcianu, A.: Notes on abstract interpretation (2001), http://www.mit.edu/~salcianu (Unpublished Manuscript)
Sen, R., Srikant, Y.N.: Executable analysis using abstract interpretation with circular linear progressions. In: Proceedings of the Fifth IEEE/ACM International Conference on Formal Methods and Models for Codesign, pp. 39–48. IEEE (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gange, G., Navas, J.A., Schachte, P., Søndergaard, H., Stuckey, P.J. (2013). Abstract Interpretation over Non-lattice Abstract Domains. In: Logozzo, F., Fähndrich, M. (eds) Static Analysis. SAS 2013. Lecture Notes in Computer Science, vol 7935. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38856-9_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-38856-9_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38855-2
Online ISBN: 978-3-642-38856-9
eBook Packages: Computer ScienceComputer Science (R0)