Skip to main content
SpringerLink
Log in

Existential Heap Abstraction Entailment Is Undecidable

  • Conference paper
  • First Online:
Book cover Static Analysis (SAS 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2694))

Included in the following conference series:

Abstract

In this paper we study constraints for specifying properties of data structures consisting of linked objects allocated in the heap. Motivated by heap summary graphs in role analysis and shape analysis we introduce the notion of regular graph constraints. A regular graph constraint is a graph representing the heap summary; a heap satisfies a constraint if and only if the heap can be homomorphically mapped to the summary. Regular graph constraints form a very simple and natural fragment of the existential monadic second-order logic over graphs. One of the key problems in a compositional static analysis is proving that procedure preconditions are satisfied at every call site. For role analysis, precondition checking requires determining the validity of implication, i.e., entailment of regular graph constraints.

The central result of this paper is the undecidability of regular graph constraint entailment. The undecidability of the entailment problem is surprising because of the simplicity of regular graph constraints: in particular, the satisfiability of regular graph constraints is decidable.

Our undecidability result implies that there is no complete algorithm for statically checking procedure preconditions or postconditions, simplifying static analysis results, or checking that given analysis results are correct. While incomplete conservative algorithms for regular graph constraint entailment checking are possible, we argue that heap specification languages should avoid second-order existential quantification in favor of explicitly specifying a criterion for summarizing objects.

This research was supported in part by DARPA Contract F33615-00-C-1692, NSF Grant CCR00-86154, NSF Grant CCR00-63513, and the Singapore-MIT Alliance.

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. Michael Benedikt, Thomas Reps, and Mooly Sagiv. A decidable logic for linked data structures. In Proc. 8th European Symposium on Programming, 1999.

    Google Scholar 

  2. Egon Börger, Erich Gräedel, and Yuri Gurevich. The Classical Decision Problem. Springer-Verlag, 1997.

    Google Scholar 

  3. Cristiano Calcagno, Luca Cardelli, and Andrew D. Gordon. Deciding validity in a spatial logic for trees. Submitted, September 2002.

    Google Scholar 

  4. Venkatesan T. Chakaravarthy and Susan B. Horwitz. On the non-approximability of points-to analysis. Acta Informatica, 38(8):587–598, June 2002.

    Article  MATH  MathSciNet  Google Scholar 

  5. David R. Chase, Mark Wegman, and F. Kenneth Zadeck. Analysis of pointers and structures. In Proc. ACM PLDI, 1990.

    Google Scholar 

  6. H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree automata techniques and applications. Available on: http://www.grappa.univ-lille3.fr/tata, 1997. release 1 October 2002.

    Google Scholar 

  7. Bruno Courcelle. The expression of graph properties and graph transformations in monadic second-order logic. In Handbook of graph grammars and computing by graph transformations, Vol. 1: Foundations, chapter 5. World Scientific, 1997.

    Google Scholar 

  8. Manuvir Das, Sorin Lerner, and Mark Seigle. ESP: Path-sensitive program verification in polynomial time. In Proc. ACM PLDI, 2002.

    Google Scholar 

  9. Robert DeLine and Manuel Fähndrich. Enforcing high-level protocols in low-level software. In Proc. ACM PLDI, 2001.

    Google Scholar 

  10. S. Drossopoulou, F. Damiani, M. Dezani-Ciancaglini, and P. Giannini. Fickle: Dynamic object re-classification. In Proc. 15th European Conference on Object-Oriented Programming, LNCS 2072, pages 130–149. Springer, 2001.

    Google Scholar 

  11. Dawson Engler, Benjamin Chelf, Andy Chou, and Seth Hallem. Checking system rules using systemspecific, programmer-written compiler extensions. In Proc. 4th USENIX Symposium on Operating Systems Design and Implementation, 2000.

    Google Scholar 

  12. Ronald Fagin, Larry J. Stockmeyer, and Moshe Y. Vardi. On monadic NP vs monadic co-NP. Information and Computation, 120(1), 1995.

    Google Scholar 

  13. Cormac Flanagan, K. Rustan M. Leino, Mark Lilibridge, Greg Nelson, James B. Saxe, and Raymie Stata. Extended Static Checking for Java. In Proc. ACM PLDI, 2002.

    Google Scholar 

  14. Jeffrey S. Foster, Tachio Terauchi, and Alex Aiken. Flow-sensitive type qualifiers. In Proc. ACM PLDI, 2002.

    Google Scholar 

  15. Pascal Fradet and Daniel Le Metayer. Shape types. In Proc. 24th ACM POPL, 1997.

    Google Scholar 

  16. Rakesh Ghiya and Laurie Hendren. Is it a tree, a DAG, or a cyclic graph? In Proc. 23rd ACM POPL, 1996.

    Google Scholar 

  17. Dora Giammarresi and Antonio Restivo. Two-dimensional languages. In Grzegorz Rozenberg and Arto Salomaa, editors, Handbook of Formal Languages Vol.3: Beyond Words. Springer-Verlag, 1997.

    Google Scholar 

  18. Wilfrid Hodges. Model Theory, volume 42 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1993.

    Google Scholar 

  19. Neil Immerman. Descriptive Complexity. Springer-Verlag, 1998.

    Google Scholar 

  20. Daniel Jackson. Alloy: A lightweight object modelling notation. Technical Report 797, MIT Laboratory for Computer Science, 2000.

    Google Scholar 

  21. Viktor Kuncak, Patrick Lam, and Martin Rinard. Role analysis. In Proc. 29th ACM POPL, 2002.

    Google Scholar 

  22. Viktor Kuncak and Martin Rinard. Typestate checking and regular graph constraints. Technical Report 863, MIT Laboratory for Computer Science, 2002. http://www.mit.edu/~vkuncak/papers/index.html.

    Google Scholar 

  23. James R. Larus and Paul N. Hilfinger. Detecting conflicts between structure accesses. In Proc. ACM PLDI, Atlanta, GA, June 1988.

    Google Scholar 

  24. Anders Møller and Michael I. Schwartzbach. The Pointer Assertion Logic Engine. In Proc. ACM PLDI, 2001.

    Google Scholar 

  25. Greg Nelson. Techniques for program verification. Technical report, XEROX Palo Alto Research Center, 1981.

    Google Scholar 

  26. Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. Principles of Program Analysis. Springer-Verlag, 1999.

    Google Scholar 

  27. Ganesan Ramalingam. The undecidability of aliasing. ACM Transactions on Programming Languages and Systems (TOPLAS), 16(5):1467–1471, 1994.

    Article  Google Scholar 

  28. H. G. Rice. Classes of recursively enumerable sets and their decision problems. Transactions of the American Mathematical Society, 89:25–29, 1953.

    MathSciNet  Google Scholar 

  29. Neil Robertson and Paul D. Seymour. Graph minors: A survey. In Ian Anderson, editor, Surveys in Combinatorics Papers for the London Math. Soc. Lecture Note Series, 1985.

    Google Scholar 

  30. Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Solving shape-analysis problems in languages with destructive updating. ACM TOPLAS, 20(1):1–50, 1998.

    Article  Google Scholar 

  31. Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Parametric shape analysis via 3-valued logic. ACM TOPLAS, 24(3):217–298, 2002.

    Article  Google Scholar 

  32. Michael Sipser. Introduction to the Theory of Computation. PWS Publishing Company, 1997.

    Google Scholar 

  33. F. Smith, D. Walker, and G. Morrisett. Alias types. In Proc. 9th European Symposium on Programming, Berlin, Germany, March 2000.

    Google Scholar 

  34. Robert E. Strom and Shaula Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering, January 1986.

    Google Scholar 

  35. Wolfgang Thomas. Languages, automata, and logic. In Handbook of Formal Languages Vol.3: Beyond Words. Springer-Verlag, 1997.

    Google Scholar 

  36. David Walker and Greg Morrisett. Alias types for recursive data structures. In Workshop on Types in Compilation, 2000.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MA, 02139

    Viktor Kuncak & Martin Rinard

Authors
  1. Viktor Kuncak
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Martin Rinard
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. École Polytechnique, STIX, 91128, Palaiseau cedex, France

    Radhia Cousot

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kuncak, V., Rinard, M. (2003). Existential Heap Abstraction Entailment Is Undecidable. In: Cousot, R. (eds) Static Analysis. SAS 2003. Lecture Notes in Computer Science, vol 2694. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44898-5_24

Download citation

  • DOI: https://doi.org/10.1007/3-540-44898-5_24

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40325-8

  • Online ISBN: 978-3-540-44898-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation