{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,6]],"date-time":"2026-04-06T10:19:00Z","timestamp":1775470740896,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540733676","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73368-3_22","type":"book-chapter","created":{"date-parts":[[2007,8,29]],"date-time":"2007-08-29T18:29:34Z","timestamp":1188412174000},"page":"178-192","source":"Crossref","is-referenced-by-count":93,"title":["Shape Analysis for Composite Data Structures"],"prefix":"10.1007","author":[{"given":"Josh","family":"Berdine","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cristiano","family":"Calcagno","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Byron","family":"Cook","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dino","family":"Distefano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter W.","family":"O\u2019Hearn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Wies","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hongseok","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_5","volume-title":"Programming Languages and Systems","author":"J. Berdine","year":"2005","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, Springer, Heidelberg (2005)"},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"Programming Languages and Systems","author":"B. Biering","year":"2005","unstructured":"Biering, B., Birkedal, L., Torp-Smith, N.: BI hyperdoctrines and higher-order separation logic. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, Springer, Heidelberg (2005)"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_5","volume-title":"Static Analysis","author":"A. Bouajjani","year":"2006","unstructured":"Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract tree regular model checking of complex dynamic data structures. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, Springer, Heidelberg (2006)"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Distefano","year":"2006","unstructured":"Distefano, D., O\u2019Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, Springer, Heidelberg (2006)"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In: PLDI (to appear, 2007)","DOI":"10.1145\/1250734.1250765"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Hackett, B., Rugina, R.: Region-based shape analysis with tracked locations. In: POPL (2005)","DOI":"10.1145\/1040305.1040331"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Programming Languages and Systems","author":"O. Lee","year":"2005","unstructured":"Lee, O., Yang, H., Yi, K.: Automatic verification of pointer programs using grammar-based shape analysis. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, Springer, Heidelberg (2005)"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_49","volume-title":"Computer Aided Verification","author":"T. Lev-Ami","year":"2006","unstructured":"Lev-Ami, T., Immerman, N., Sagiv, M.: Abstraction for shape analysis with fast and precise transfomers. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, Springer, Heidelberg (2006)"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"Static Analysis","author":"T. Lev-Ami","year":"2000","unstructured":"Lev-Ami, T., Sagiv, M.: A system for implementing static analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, Springer, Heidelberg (2000)"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"A. Loginov","year":"2005","unstructured":"Loginov, A., Reps, T., Sagiv, M.: Abstraction refinement via inductive learning. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, Springer, Heidelberg (2005)"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R. Manevich","year":"2005","unstructured":"Manevich, R., Yahav, E., Ramalingam, G., Sagiv, M.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, Springer, Heidelberg (2005)"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_19","volume-title":"Static Analysis","author":"A. Podelski","year":"2005","unstructured":"Podelski, A., Wies, T.: Boolean heaps. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, Springer, Heidelberg (2005)"},{"key":"22_CR13","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS (2002)"},{"key":"22_CR14","unstructured":"Rinetzky, N., Ramalingam, G., Sagiv, M., Yahav, E.: Componentized heap abstraction. TR-164\/06, School of Computer Science, Tel Aviv Univ. (December 2006)"},{"issue":"1","key":"22_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/271510.271517","volume":"20","author":"M. Sagiv","year":"1998","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Solving shape-analysis problems in languages with destructive updating. ACM TOPLAS\u00a020(1), 1\u201350 (1998)","journal-title":"ACM TOPLAS"},{"issue":"3","key":"22_CR16","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM TOPLAS\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM TOPLAS"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"\u010ce\u0161ka, M., Erlebach, P., Vojnar, T.: Generalised multi-pattern-based verification of programs with linear linked structures. Formal Aspects Comput. (2007)","DOI":"10.1007\/s00165-007-0031-x"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73368-3_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:08:27Z","timestamp":1619503707000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73368-3_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540733676"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73368-3_22","relation":{},"subject":[]}}