{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T08:01:57Z","timestamp":1767772917017},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540697350"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-69738-1_7","type":"book-chapter","created":{"date-parts":[[2007,11,12]],"date-time":"2007-11-12T07:58:07Z","timestamp":1194854287000},"page":"91-105","source":"Crossref","is-referenced-by-count":15,"title":["Shape Analysis of Single-Parent Heaps"],"prefix":"10.1007","author":[{"given":"Ittai","family":"Balaban","sequence":"first","affiliation":[]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[]},{"given":"Lenore D.","family":"Zuck","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1007\/3-540-44585-4_19","volume-title":"Computer Aided Verification","author":"T. Arons","year":"2001","unstructured":"Arons, T., et al.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 221\u2013234. Springer, Heidelberg (2001)"},{"key":"7_CR2","unstructured":"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)"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1007\/978-3-540-30579-8_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"I. Balaban","year":"2005","unstructured":"Balaban, I., Pnueli, A., Zuck, L.D.: Shape analysis by predicate abstraction. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 164\u2013180. Springer, Heidelberg (2005)"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1142\/S0129054107004553"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","first-page":"17","volume-title":"Computer Aided Verification","year":"2006","unstructured":"Ball, T., Jones, R.B. (eds.): CAV 2006. LNCS, vol.\u00a04144, pp. 17\u201320. Springer, Heidelberg (2006)"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-49099-X_2","volume-title":"Programming Languages and Systems","author":"M. Benedikt","year":"1999","unstructured":"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\u201319. Springer, Berlin Heidelberg New York (1999)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/11817963_35","volume-title":"Computer Aided Verification","author":"J. Berdine","year":"2006","unstructured":"Berdine, J., et al.: Automatic termination proofs for programs with shape-shifting heaps. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 386\u2013400. Springer, Heidelberg (2006)"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/11609773_14","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J.D. Bingham","year":"2005","unstructured":"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.\u00a03855, pp. 207\u2013221. Springer, Heidelberg (2005)"},{"key":"7_CR9","volume-title":"Perspectives of Mathematical Logic","author":"E. B\u00f6rger","year":"2001","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The Classical Decision Problem. In: Perspectives of Mathematical Logic, 2nd edn., Springer, New York (2001)","edition":"2"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/11817963_47","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2006","unstructured":"Bouajjani, A., et al.: Programs with lists are counter automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 517\u2013531. Springer, Heidelberg (2006)"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/BFb0023464","volume-title":"STACS 97","author":"E. Gr\u00e4del","year":"1997","unstructured":"Gr\u00e4del, E., Otto, M., Rosen, E.: Undecidability results on two-variable logics. In: Reischuk, R., Morvan, M. (eds.) STACS 97. LNCS, vol.\u00a01200, pp. 249\u2013260. Springer, Heidelberg (1997)"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1007\/978-3-540-30124-0_15","volume-title":"Computer Science Logic","author":"N. Immerman","year":"2004","unstructured":"Immerman, N., et al.: The boundary between decidability and undecidability for transitive-closure logics. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, pp. 160\u2013174. Springer, Heidelberg (2004)"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1007\/978-3-540-27813-9_22","volume-title":"Computer Aided Verification","author":"N. Immerman","year":"2004","unstructured":"Immerman, N., et al.: Verification via structure simulation. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 281\u2013294. Springer, Heidelberg (2004)"},{"issue":"1","key":"7_CR14","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1006\/inco.2000.3000","volume":"163","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. Information and Computation\u00a0163(1), 203\u2013243 (2000)","journal-title":"Information and Computation"},{"key":"7_CR15","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1145\/158511.158628","volume-title":"POPL \u201993: Proceedings of the 2th ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"N. Klarlund","year":"1993","unstructured":"Klarlund, N., Schwartzbach, M.I.: Graph types. In: POPL \u201993: Proceedings of the 2th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 196\u2013205. ACM Press, New York (1993)"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1007\/978-3-540-30579-8_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R. Manevich","year":"2005","unstructured":"Manevich, R., et al.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 181\u2013198. Springer, Heidelberg (2005)"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The Pointer Assertion Logic Engine. In: Programming Language Design and Implementation (2001)","DOI":"10.1145\/378795.378851"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/3-540-61474-5_68","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"1996","unstructured":"Pnueli, A., Shahar, E.: A platform combining deductive with algorithmic verification. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, p. 184. Springer, Heidelberg (1996)"},{"key":"7_CR19","first-page":"55","volume-title":"LICS","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55\u201374. IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Wies, T., et al.: On field constraint analysis. In: Verification, Model Checking, and Abstract Interpretation (2006)","DOI":"10.1007\/11609773_11"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/11690634_7","volume-title":"Foundations of Software Science and Computation Structures","author":"G. Yorsh","year":"2006","unstructured":"Yorsh, G., et al.: A logic of reachable patterns in linked data-structures. In: Aceto, L., Ing\u00f3lfsd\u00f3ttir, A. (eds.) FOSSACS 2006 and ETAPS 2006. LNCS, vol.\u00a03921, pp. 94\u2013110. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69738-1_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T00:45:11Z","timestamp":1620002711000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69738-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540697350"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69738-1_7","relation":{},"subject":[]}}