Advertisement

Shape Analysis of Single-Parent Heaps

  • Ittai Balaban
  • Amir Pnueli
  • Lenore D. Zuck
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4349)

Abstract

We define the class of single-parent heap systems, which rely on a singly-linked heap in order to model destructive updates on tree structures. This encoding has the advantage of relying on a relatively simple theory of linked lists in order to support abstraction computation. To facilitate the application of this encoding, we provide a program transformation that, given a program operating on a multi-linked heap without sharing, transforms it into one over a single-parent heap. It is then possible to apply shape analysis by predicate and ranking abstraction as in [3]. The technique has been successfully applied on examples with trees of fixed arity (balancing of and insertion into a binary sort tree).

Keywords

Index Variable Transition Relation Atomic Formula Predicate Abstraction Index Array 
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.
    Arons, T., et al.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 221–234. Springer, Heidelberg (2001)Google Scholar
  2. 2.
    Balaban, I., Pnueli, A., Zuck, L.: Shape analysis of single-parent heaps. Research Report TR2006-885, Computer Science Department, New York University, Warren Weaver Hall, Room 405, 251 Mercer St., New York, NY 10012 (November 2006)Google Scholar
  3. 3.
    Balaban, I., Pnueli, A., Zuck, L.D.: Shape analysis by predicate abstraction. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 164–180. Springer, Heidelberg (2005)Google Scholar
  4. 4.
    Balaban, I., Pnueli, A., Zuck, L.D.: Modular ranking abstraction. To appear in International Journal of Foundations of Computer Science IJFCS (2007), See http://www.cs.nyu.edu/acsys/pubs/permanent/ranking-companion-pre.pdf
  5. 5.
    Ball, T., Jones, R.B. (eds.): CAV 2006. LNCS, vol. 4144, pp. 17–20. Springer, Heidelberg (2006)zbMATHGoogle Scholar
  6. 6.
    Benedikt, M., Reps, T.W., Sagiv, S.: A decidable logic for describing linked data structures. In: Swierstra, S.D. (ed.) ESOP 1999 and ETAPS 1999. LNCS, vol. 1576, pp. 2–19. Springer, Berlin Heidelberg New York (1999)CrossRefGoogle Scholar
  7. 7.
    Berdine, J., et al.: Automatic termination proofs for programs with shape-shifting heaps. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 386–400. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  8. 8.
    Bingham, J.D., Rakamaric, Z.: A logic and decision procedure for predicate abstraction of heap-manipulating programs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 207–221. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  9. 9.
    Börger, E., Grädel, E., Gurevich, Y.: The Classical Decision Problem. In: Perspectives of Mathematical Logic, 2nd edn., Springer, New York (2001)Google Scholar
  10. 10.
    Bouajjani, A., et al.: Programs with lists are counter automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 517–531. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  11. 11.
    Grädel, E., Otto, M., Rosen, E.: Undecidability results on two-variable logics. In: Reischuk, R., Morvan, M. (eds.) STACS 97. LNCS, vol. 1200, pp. 249–260. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  12. 12.
    Immerman, N., et al.: The boundary between decidability and undecidability for transitive-closure logics. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 160–174. Springer, Heidelberg (2004)Google Scholar
  13. 13.
    Immerman, N., et al.: Verification via structure simulation. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 281–294. Springer, Heidelberg (2004)Google Scholar
  14. 14.
    Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. Information and Computation 163(1), 203–243 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    Klarlund, N., Schwartzbach, M.I.: Graph types. In: POPL ’93: Proceedings of the 2th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 196–205. ACM Press, New York (1993)CrossRefGoogle Scholar
  16. 16.
    Manevich, R., et al.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 181–198. Springer, Heidelberg (2005)Google Scholar
  17. 17.
    Møller, A., Schwartzbach, M.I.: The Pointer Assertion Logic Engine. In: Programming Language Design and Implementation (2001)Google Scholar
  18. 18.
    Pnueli, A., Shahar, E.: A platform combining deductive with algorithmic verification. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, p. 184. Springer, Heidelberg (1996)Google Scholar
  19. 19.
    Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55–74. IEEE Computer Society Press, Los Alamitos (2002)Google Scholar
  20. 20.
    Wies, T., et al.: On field constraint analysis. In: Verification, Model Checking, and Abstract Interpretation (2006)Google Scholar
  21. 21.
    Yorsh, G., et al.: A logic of reachable patterns in linked data-structures. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006 and ETAPS 2006. LNCS, vol. 3921, pp. 94–110. Springer, Heidelberg (2006)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Ittai Balaban
    • 1
  • Amir Pnueli
    • 1
    • 2
  • Lenore D. Zuck
    • 3
  1. 1.New York University, New York 
  2. 2.Weizmann Institute of Science 
  3. 3.University of Illinois at Chicago 

Personalised recommendations