Skip to main content
SpringerLink
Log in

A Posteriori Soundness for Non-deterministic Abstract Interpretations

  • Conference paper
Verification, Model Checking, and Abstract Interpretation (VMCAI 2009)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5403))

Abstract

An abstract interpretation’s resource-allocation policy (e.g., one heap summary node per allocation site) largely determines both its speed and precision. Historically, context has driven allocation policies, and as a result, these policies are said to determine the “context-sensitivity” of the analysis. This work gives analysis designers newfound freedom to manipulate speed and precision by severing the link between allocation policy and context-sensitivity: abstract allocation policies may be unhinged not only from context, but also from even a predefined correspondence with a concrete allocation policy. We do so by proving that abstract allocation policies can be made non-deterministic without sacrificing correctness; this non-determinism permits precision-guided allocation policies previously assumed to be unsafe. To prove correctness, we introduce the notion of a posteriori soundness for an analysis. A proof of a posteriori soundness differs from a standard proof of soundness in that the abstraction maps used in an a posteriori proof cannot be constructed until after an analysis has been run. Delaying construction allows them to be built so as to justify the decisions made by non-determinism. The crux of the a posteriori soundness theorem is to demonstrate that a justifying abstraction map can always be constructed.

This research was funded in part by NASA Cooperative Agreement NNX08AE37A and NSF grants CCF-0429924, IIS-0417413, and CCF-0438871.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Agesen, O.: The cartesian product algorithm: Simple and precise type inference of parametric polymorphism. In: Olthoff, W. (ed.) ECOOP 1995. LNCS, vol. 952, pp. 2–26. Springer, Heidelberg (1995)

    Google Scholar 

  2. Andersen, L.O.: Program Analysis and Specialization for the C Programming Language. PhD thesis, DIKU, University of Copenhagen (May 1994)

    Google Scholar 

  3. Balakrishnan, G., Reps, T.: Recency-abstraction for heap-allocated storage. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 221–239. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  4. Chase, D.R., Wegman, M., Zadeck, F.K.: Analysis of Pointers and Structures. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, White Plains, New York, June 1990, pp. 296–310 (1990)

    Google Scholar 

  5. Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Electronic Notes in Theoretical Computer Science 6, 25 pages (1997), http://www.elsevier.nl/locate/entcs/volume6.html

  6. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Los Angeles, California, pp. 238–252. ACM Press, New York (1977)

    Chapter  Google Scholar 

  7. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, Texas, pp. 269–282. ACM Press, New York (1979)

    Chapter  Google Scholar 

  8. Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation 2(4), 511–547 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  9. Gallagher, J., Gallagher, J.P., Puebla, G., Puebla, G.: Abstract interpretation over non-deterministic finite tree automata for set-based analysis of logic programs. In: Krishnamurthi, S., Ramakrishnan, C.R. (eds.) PADL 2002. LNCS, vol. 2257, pp. 243–261. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  10. Gulwani, S.: Program analysis using random interpretation. Ph.D. Dissertation, UC-Berkeley (2005)

    Google Scholar 

  11. Harrison, W.L.: The interprocedural analysis and automatic parallelization of Scheme programs. Lisp and Symbolic Computation 2(3/4), 179–396 (1989)

    Article  Google Scholar 

  12. Hudak, P.: A semantic model of reference counting and its abstraction (detailed summary). In: Proceedings of the 1986 ACM Conference on LISP and Functional Programming, Cambridge, Massachusetts, August 1986, pp. 351–363 (1986)

    Google Scholar 

  13. Huth, M.: An abstraction framework for mixed non-deterministic and probabilistic systems. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 419–444. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  14. Jagannathan, S., Thiemann, P., Weeks, S., Wright, A.K.: Single and loving it: Must-alias analysis for higher-order languages. In: Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, California, January 1998, pp. 329–341 (1998)

    Google Scholar 

  15. Jones, N.D.: Flow analysis of lambda expressions (preliminary version). In: Even, S., Kariv, O. (eds.) ICALP 1981. LNCS, vol. 115, pp. 114–128. Springer, Heidelberg (1981)

    Chapter  Google Scholar 

  16. Jones, N.D., Muchnick, S.S.: A flexible approach to interprocedural data flow analysis and programs with recursive data structures. In: Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 66–74. ACM, New York (1982)

    Google Scholar 

  17. Might, M.: Environment Analysis of Higher-Order Languages. PhD thesis, Georgia Institute of Technology (2007)

    Google Scholar 

  18. Might, M., Shivers, O.: Environment analysis via ΔCFA. In: Proceedings of the 33rd Annual ACM Symposium on the Principles of Programming Languages (POPL 2006), Charleston, South Carolina, January 2006, pp. 127–140 (2006)

    Google Scholar 

  19. Might, M., Shivers, O.: Improving flow analyses via ΓCFA: Abstract garbage collection and counting. In: Proceedings of the 11th ACM International Conference on Functional Programming (ICFP 2006), Portland, Oregon, September 2006, pp. 13–25 (2006)

    Google Scholar 

  20. Might, M., Shivers, O.: Analyzing the environment structure of higher-order languages using frame strings. Theoretical Computer Science 375(1–3), 137–168 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  21. Might, M., Shivers, O.: Exploiting reachability and cardinality in abstract interpretation. Journal of Functional Programming (2008)

    Google Scholar 

  22. Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: Symposium on Principles of Programming Languages, pp. 105–118 (1999)

    Google Scholar 

  23. Shivers, O.: Control-flow analysis in Scheme. In: Proceedings of the SIGPLAN 1988 Conference on Programming Language Design and Implementation (PLDI), Atlanta, Georgia, June 1988, pp. 164–174 (1988)

    Google Scholar 

  24. Shivers, O.: Control-Flow Analysis of Higher-Order Languages. PhD thesis, School of Computer Science, Carnegie-Mellon University, Pittsburgh, Pennsylvania, Technical Report CMU-CS-91-145 (May 1991)

    Google Scholar 

  25. Wright, A.K., Jagannathan, S.: Polymorphic splitting: An effective polyvariant flow analysis. ACM Transactions on Programming Languages and Systems 20(1), 166–207 (1998)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Utah, Salt Lake City, Utah, USA

    Matthew Might

  2. Northeastern University, Boston, Massachusetts, USA

    Panagiotis Manolios

Authors
  1. Matthew Might
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Panagiotis Manolios
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. (Emeritus University of Copenhagen), Bukkeballevej 88, 2960, Rungsted, Denmark

    Neil D. Jones

  2. Institut für Informatik, Fachbereich Mathematik und Informatik, Westfälische Wilhelms-Universität, 48149, Münster, Germany

    Markus Müller-Olm

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Might, M., Manolios, P. (2008). A Posteriori Soundness for Non-deterministic Abstract Interpretations. In: Jones, N.D., Müller-Olm, M. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2009. Lecture Notes in Computer Science, vol 5403. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-93900-9_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-93900-9_22

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-93899-6

  • Online ISBN: 978-3-540-93900-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation