{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:43:23Z","timestamp":1770291803777,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540374060","type":"print"},{"value":"9783540374114","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11817963_35","type":"book-chapter","created":{"date-parts":[[2006,8,5]],"date-time":"2006-08-05T05:07:51Z","timestamp":1154754471000},"page":"386-400","source":"Crossref","is-referenced-by-count":70,"title":["Automatic Termination Proofs for Programs with Shape-Shifting Heaps"],"prefix":"10.1007","author":[{"given":"Josh","family":"Berdine","sequence":"first","affiliation":[]},{"given":"Byron","family":"Cook","sequence":"additional","affiliation":[]},{"given":"Dino","family":"Distefano","sequence":"additional","affiliation":[]},{"given":"Peter W.","family":"O\u2019Hearn","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"35_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","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, pp. 52\u201368. Springer, Heidelberg (2005)"},{"key":"35_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-30579-8_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Bradley","year":"2005","unstructured":"Bradley, A., Manna, Z., Sipma, H.: Termination of polynomial programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 113\u2013129. Springer, Heidelberg (2005)"},{"key":"35_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/11547662_8","volume-title":"Static Analysis","author":"B. Cook","year":"2005","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Abstraction refinement for termination. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 87\u2013101. Springer, Heidelberg (2005)"},{"key":"35_CR4","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI (2006)","DOI":"10.1145\/1133981.1134029"},{"key":"35_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/11817963_37","volume-title":"Computer Aided Verification","author":"B. Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Terminator: Beyond safety. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 415\u2013418. Springer, Heidelberg (2006)"},{"key":"35_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-540-30538-5_21","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"D. Distefano","year":"2004","unstructured":"Distefano, D., Katoen, J.-P., Rensink, A.: Who is pointing when to whom? on the automated verification of linked list structures. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 250\u2013262. Springer, Heidelberg (2004)"},{"key":"35_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","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. LNCS, vol.\u00a03920, pp. 287\u2013302. Springer, Heidelberg (2006)"},{"key":"35_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-540-45099-3_7","volume-title":"Static Analysis","author":"N. Dor","year":"2000","unstructured":"Dor, N., Rodeh, M., Sagiv, S.: Checking cleanness in linked lists. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, pp. 115\u2013135. Springer, Heidelberg (2000)"},{"key":"35_CR9","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Proceedings of Symposia in Applied Mathematics (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"35_CR10","doi-asserted-by":"crossref","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: POPL (2001)","DOI":"10.1145\/360204.360210"},{"key":"35_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 239\u2013251. Springer, Heidelberg (2004)"},{"key":"35_CR12","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"35_CR13","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. In: POPL (2005)","DOI":"10.1145\/1040305.1040317"},{"key":"35_CR14","unstructured":"Reynolds, J.: Separation logic: A logic for shared mutable data structures. In: LICS (2002)"},{"key":"35_CR15","unstructured":"Yahav, E.: Property-Guided Verification of Concurrent Heap-Manipulating Programs. PhD thesis (2004)"},{"key":"35_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/3-540-36575-3_15","volume-title":"Programming Languages and Systems","author":"E. Yahav","year":"2003","unstructured":"Yahav, E., Reps, T., Sagiv, M., Wilhelm, R.: Verifying temporal heap properties specified via evolution logic. In: Degano, P. (ed.) ESOP 2003. LNCS, vol.\u00a02618, pp. 204\u2013222. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11817963_35.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:30:04Z","timestamp":1619508604000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11817963_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540374060","9783540374114"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/11817963_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}