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).
This research was supported in part by ONR grant N00014-99-1-0131, and SRC grant 2004-TJ-1256.
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
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)
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)
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)
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
Ball, T., Jones, R.B. (eds.): CAV 2006. LNCS, vol. 4144, pp. 17–20. Springer, Heidelberg (2006)
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)
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)
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)
Börger, E., Grädel, E., Gurevich, Y.: The Classical Decision Problem. In: Perspectives of Mathematical Logic, 2nd edn., Springer, New York (2001)
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)
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)
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)
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)
Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. Information and Computation 163(1), 203–243 (2000)
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)
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)
Møller, A., Schwartzbach, M.I.: The Pointer Assertion Logic Engine. In: Programming Language Design and Implementation (2001)
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)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55–74. IEEE Computer Society Press, Los Alamitos (2002)
Wies, T., et al.: On field constraint analysis. In: Verification, Model Checking, and Abstract Interpretation (2006)
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)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Balaban, I., Pnueli, A., Zuck, L.D. (2007). Shape Analysis of Single-Parent Heaps. In: Cook, B., Podelski, A. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2007. Lecture Notes in Computer Science, vol 4349. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69738-1_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-69738-1_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69735-0
Online ISBN: 978-3-540-69738-1
eBook Packages: Computer ScienceComputer Science (R0)