{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T10:36:36Z","timestamp":1777890996212,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642385735","type":"print"},{"value":"9783642385742","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38574-2_2","type":"book-chapter","created":{"date-parts":[[2013,6,4]],"date-time":"2013-06-04T07:55:13Z","timestamp":1370332513000},"page":"21-38","source":"Crossref","is-referenced-by-count":77,"title":["The Tree Width of Separation Logic with Recursive Definitions"],"prefix":"10.1007","author":[{"given":"Radu","family":"Iosif","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adam","family":"Rogalewicz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jiri","family":"Simacek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-540-73368-3_22","volume-title":"Computer Aided Verification","author":"J. Berdine","year":"2007","unstructured":"Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.W., Wies, T., Yang, H.: Shape analysis for composite data structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 178\u2013192. Springer, Heidelberg (2007)"},{"key":"2_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)"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-88282-4_1","volume-title":"Language and Automata Theory and Applications","author":"M. Boja\u0144czyk","year":"2008","unstructured":"Boja\u0144czyk, M.: Tree-walking automata. In: Mart\u00edn-Vide, C., Otto, F., Fernau, H. (eds.) LATA 2008. LNCS, vol.\u00a05196, pp. 1\u20132. Springer, Heidelberg (2008)"},{"key":"2_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)"},{"issue":"2","key":"2_CR5","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/s10817-010-9179-9","volume":"45","author":"M. Bozga","year":"2010","unstructured":"Bozga, M., Iosif, R., Perarnau, S.: Quantitative separation logic and programs with lists. J. Autom. Reasoning\u00a045(2), 131\u2013156 (2010)","journal-title":"J. Autom. Reasoning"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Kanovich, M.: Undecidability of propositional separation logic and its neighbours. In: Proceedings of the 2010 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, pp. 130\u2013139 (2010)","DOI":"10.1109\/LICS.2010.24"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/978-3-642-20398-5_33","volume-title":"NASA Formal Methods","author":"C. Calcagno","year":"2011","unstructured":"Calcagno, C., Distefano, D.: Infer: An automatic program verifier for memory safety of C programs. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 459\u2013465. Springer, Heidelberg (2011)"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-642-23217-6_16","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"B. Cook","year":"2011","unstructured":"Cook, B., Haase, C., Ouaknine, J., Parkinson, M., Worrell, J.: Tractable reasoning in a fragment of separation logic. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol.\u00a06901, pp. 235\u2013249. Springer, Heidelberg (2011)"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-642-22110-1_29","volume-title":"Computer Aided Verification","author":"K. Dudka","year":"2011","unstructured":"Dudka, K., Peringer, P., Vojnar, T.: Predator: A practical tool for checking manipulation of dynamic data structures using separation logic. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 372\u2013378. Springer, Heidelberg (2011)"},{"key":"2_CR10","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1007\/978-3-642-37036-6_9","volume-title":"Programming Languages and Systems","author":"Constantin Enea","year":"2013","unstructured":"Enea, C., Saveluc, V., Sighireanu, M.: Compositional invariant checking for overlaid and nested linked lists. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol.\u00a07792, pp. 129\u2013148. Springer, Heidelberg (2013)"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: 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":"2_CR12","doi-asserted-by":"crossref","unstructured":"Iosif, R., Rogalewicz, A., Simacek, J.: The tree width of separation logic with recursive definitions. CoRR abs\/1301.5139 (2013)","DOI":"10.1007\/978-3-642-38574-2_2"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Parlato, G.: The tree width of auxiliary storage. In: Proc. of POPL 2011. ACM (2011)","DOI":"10.1145\/1926385.1926419"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Parlato, G., Qiu, X.: Decidable logics combining heap structures and data. In: Proc. of POPL 2011 (2011)","DOI":"10.1145\/1926385.1926455"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: Proc. of PLDI 2001 (June 2001)","DOI":"10.1145\/378795.378851"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-70545-1_34","volume-title":"Computer Aided Verification","author":"H.H. Nguyen","year":"2008","unstructured":"Nguyen, H.H., Chin, W.-N.: Enhancing program verification with lemmas. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 355\u2013369. Springer, Heidelberg (2008)"},{"key":"2_CR17","unstructured":"Reynolds, J.: Separation Logic: A Logic for Shared Mutable Data Structures. In: Proc. of LICS 2002. IEEE CS Press (2002)"},{"issue":"2","key":"2_CR18","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/0168-0072(91)90054-P","volume":"53","author":"D. Seese","year":"1991","unstructured":"Seese, D.: The structure of models of decidable monadic theories of graphs. Annals of Pure and Applied Logic\u00a053(2), 169\u2013195 (1991)","journal-title":"Annals of Pure and Applied Logic"},{"key":"2_CR19","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., 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 Deduction \u2013 CADE-24"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38574-2_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,14]],"date-time":"2019-07-14T15:11:19Z","timestamp":1563117079000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38574-2_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642385735","9783642385742"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38574-2_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}