{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T15:26:10Z","timestamp":1772119570151,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540240587","type":"print"},{"value":"9783540305385","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30538-5_9","type":"book-chapter","created":{"date-parts":[[2010,3,12]],"date-time":"2010-03-12T13:40:30Z","timestamp":1268401230000},"page":"97-109","source":"Crossref","is-referenced-by-count":130,"title":["A Decidable Fragment of Separation Logic"],"prefix":"10.1007","author":[{"given":"Josh","family":"Berdine","sequence":"first","affiliation":[]},{"given":"Cristiano","family":"Calcagno","sequence":"additional","affiliation":[]},{"given":"Peter W.","family":"O\u2019Hearn","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","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, Los Alamitos (2002)"},{"key":"9_CR2","unstructured":"Reynolds, J.C.: Intuitionistic reasoning about shared mutable data structure. In: Davies, J., Roscoe, B., Woodcock, J. (eds.) Millennial Perspectives in Computer Science, Houndsmill, Hampshire, Palgrave, pp. 303\u2013321 (2000)"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Isthiaq, S., O\u2019Hearn, P.: BI as an assertion language for mutable data structures. In: POPL, London, pp. 39\u201346 (2001)","DOI":"10.1145\/360204.375719"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P. O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, pp. 1\u201319. Springer, Heidelberg (2001)"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-45294-X_10","volume-title":"FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science","author":"C. Calcagno","year":"2001","unstructured":"Calcagno, C., Yang, H., O\u2019Hearn, P.: Computability and complexity results for a spatial assertion language for data structures. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol.\u00a02245, pp. 108\u2013119. Springer, Heidelberg (2001)"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: POPL, Venice, pp. 268\u2013280 (2004)","DOI":"10.1145\/964001.964024"},{"key":"9_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/1995086","volume":"141","author":"M.O. Rabin","year":"1969","unstructured":"Rabin, M.O.: Decidability of secon-order theories and automata on infinite trees. Trans. of American Math. Society\u00a0141, 1\u201335 (1969)","journal-title":"Trans. of American Math. Society"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Jenson, J., Jorgensen, M., Klarkund, N., Schwartzback, M.: Automatic verification of pointer programs using monadic second-order logic. In: PLDI, SIGPLAN Notices, vol.\u00a032(5) (1997)","DOI":"10.1145\/258916.258936"},{"key":"9_CR9","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., Sagiv, M.: A decidable logic for describing linked data structures. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol.\u00a01576, pp. 2\u201319. Springer, Heidelberg (1999)"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: Verification via structure simulation. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 281\u2013294. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30538-5_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:59:00Z","timestamp":1605761940000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30538-5_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540240587","9783540305385"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30538-5_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}