Advertisement

Abstract Interpretation over Non-lattice Abstract Domains

  • Graeme Gange
  • Jorge A. Navas
  • Peter Schachte
  • Harald Søndergaard
  • Peter J. Stuckey
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7935)

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

Partial Order Complete Lattice Abstract Interpretation Abstract Domain Index Expression 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    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)Google Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    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)CrossRefGoogle Scholar
  4. 4.
    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)Google Scholar
  5. 5.
    Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University (1990)Google Scholar
  6. 6.
    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)CrossRefGoogle Scholar
  7. 7.
    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)Google Scholar
  8. 8.
    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)Google Scholar
  9. 9.
    Halbwachs, N., Péron, M.: Discovering properties about arrays in simple programs. SIGPLAN Notices 43, 339–348 (2008)CrossRefGoogle Scholar
  10. 10.
    Knuth, D.E.: The Art of Computer Programming, 2nd edn., vol. 2. Addison-Wesley (1981)Google Scholar
  11. 11.
    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)CrossRefGoogle Scholar
  12. 12.
    Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer (1999)Google Scholar
  13. 13.
    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)Google Scholar
  14. 14.
    Sălcianu, A.: Notes on abstract interpretation (2001), http://www.mit.edu/~salcianu (Unpublished Manuscript)
  15. 15.
    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)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Graeme Gange
    • 1
  • Jorge A. Navas
    • 1
  • Peter Schachte
    • 1
  • Harald Søndergaard
    • 1
  • Peter J. Stuckey
    • 1
  1. 1.Department of Computing and Information SystemsThe University of MelbourneVictoriaAustralia

Personalised recommendations