{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,2]],"date-time":"2025-04-02T10:40:22Z","timestamp":1743590422308,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642313646"},{"type":"electronic","value":"9783642313653"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31365-3_14","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T20:35:34Z","timestamp":1340310934000},"page":"149-163","source":"Crossref","is-referenced-by-count":4,"title":["Automated Verification of Recursive Programs with Pointers"],"prefix":"10.1007","author":[{"given":"Frank","family":"de Boer","sequence":"first","affiliation":[]},{"given":"Marcello","family":"Bonsangue","sequence":"additional","affiliation":[]},{"given":"Jurriaan","family":"Rot","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","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":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-540-30538-5_9","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"J. Berdine","year":"2004","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: A Decidable Fragment of Separation Logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 97\u2013109. Springer, Heidelberg (2004)"},{"doi-asserted-by":"crossref","unstructured":"Blackburn, P., de Rijke, M., Venema, Y.: Modal logic. Cambridge University Press (2001)","key":"14_CR3","DOI":"10.1017\/CBO9781107050884"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-642-04081-8_13","volume-title":"CONCUR 2009 - Concurrency Theory","author":"A. Bouajjani","year":"2009","unstructured":"Bouajjani, A., Dr\u0103goi, C., Enea, C., Sighireanu, M.: A Logic-Based Framework for Reasoning about Composite Data Structures. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol.\u00a05710, pp. 178\u2013195. Springer, Heidelberg (2009)"},{"doi-asserted-by":"crossref","unstructured":"Brotherston, J., Kanovich, M.I.: Undecidability of propositional separation logic and its neighbours. In: LICS 2010, pp. 130\u2013139. IEEE (2010)","key":"14_CR5","DOI":"10.1109\/LICS.2010.24"},{"key":"14_CR6","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1145\/322108.322121","volume":"26","author":"E.M. Clarke","year":"1979","unstructured":"Clarke, E.M.: Programming language constructs for which it is impossible to obtain good hoare-like axioms. Journal of the ACM\u00a026, 126\u2013147 (1979)","journal-title":"Journal of the ACM"},{"doi-asserted-by":"crossref","unstructured":"Clavel, M., Eker, S., Lincoln, P., Meseguer, J.: Principles of maude. ENTCS, vol.\u00a04. Elsevier (2000)","key":"14_CR7","DOI":"10.1016\/S1571-0661(04)00034-9"},{"doi-asserted-by":"crossref","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000)","key":"14_CR8","DOI":"10.7551\/mitpress\/2516.001.0001"},{"doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Verifying properties of well-founded linked lists. In: POPL 2006, pp. 115\u2013126. ACM (2006)","key":"14_CR9","DOI":"10.1145\/1111320.1111048"},{"doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Parlato, G., Qiu, X.: Decidable logics combining heap structures and data. In: POPL 2011, pp. 611\u2013622. ACM (2011)","key":"14_CR10","DOI":"10.1145\/1925844.1926455"},{"doi-asserted-by":"crossref","unstructured":"Morris, J.M.: Assignment and linked data structures. In: Theoretical Foundations of Programming Methodology (1982)","key":"14_CR11","DOI":"10.1007\/978-94-009-7893-5_4"},{"doi-asserted-by":"crossref","unstructured":"Naumann, D.A.: Calculating sharp adaptation rules. Information Processing Letters\u00a077 (2000)","key":"14_CR12","DOI":"10.1016\/S0020-0190(00)00215-5"},{"doi-asserted-by":"crossref","unstructured":"Nelson, G.: Verifying Reachability Invariants of Linked Structures. In: POPL 1983, pp. 38\u201347. ACM (1983)","key":"14_CR13","DOI":"10.1145\/567067.567073"},{"doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS 2002, pp. 55\u201374. IEEE (2002)","key":"14_CR14","DOI":"10.1109\/LICS.2002.1029817"},{"key":"14_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/3-540-45744-5_7","volume-title":"Automated Reasoning","author":"U. Sattler","year":"2001","unstructured":"Sattler, U., Vardi, M.Y.: The hybrid \u03bc-calculus. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 76\u201391. Springer, Heidelberg (2001)"},{"doi-asserted-by":"crossref","unstructured":"Tanabe, Y., Sekizawa, T., Yuasa, Y., Takahashi, K.: Pre- and post-conditions expressed in variants of the modal \u03bc-calculus. IEICE Transactions (2009)","key":"14_CR16","DOI":"10.1587\/transinf.E92.D.995"},{"key":"14_CR17","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., Rabinovich, A.M., Sagiv, M., Meyer, A., Bouajjani, A.: A Logic of Reachable Patterns in Linked Data-Structures. In: Aceto, L., Ing\u00f3lfsd\u00f3ttir, A. (eds.) FOSSACS 2006. LNCS, vol.\u00a03921, pp. 94\u2013110. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31365-3_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,2]],"date-time":"2025-04-02T10:16:04Z","timestamp":1743588964000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31365-3_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642313646","9783642313653"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31365-3_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}