{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T12:51:45Z","timestamp":1760014305858,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642005954"},{"type":"electronic","value":"9783642005961"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-00596-1_30","type":"book-chapter","created":{"date-parts":[[2009,3,27]],"date-time":"2009-03-27T01:13:03Z","timestamp":1238116383000},"page":"425-439","source":"Crossref","is-referenced-by-count":5,"title":["Beyond Shapes: Lists with Ordered Data"],"prefix":"10.1007","author":[{"given":"Kshitij","family":"Bansal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R\u00e9mi","family":"Brochenin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Etienne","family":"Lozes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"30_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11804192_6","volume-title":"Formal Methods for Components and Objects","author":"J. Berdine","year":"2006","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.: Smallfoot: Modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 115\u2013137. Springer, Heidelberg (2006)"},{"doi-asserted-by":"crossref","unstructured":"Bojanczyk, M., Muscholl, A., Schwentick, T., Segoufin, L., David, C.: Two-variable logic on words with data. In: Proceedings of 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, pp. 7\u201316 (2006)","key":"30_CR2","DOI":"10.1109\/LICS.2006.51"},{"key":"30_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/11817963_47","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2006","unstructured":"Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with lists are counter automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 517\u2013531. Springer, Heidelberg (2006)"},{"key":"30_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/978-3-540-27864-1_25","volume-title":"Static Analysis","author":"M. Bozga","year":"2004","unstructured":"Bozga, M., Iosif, R., Lakhnech, Y.: On logics of aliasing. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 344\u2013360. Springer, Heidelberg (2004)"},{"doi-asserted-by":"crossref","unstructured":"Brochenin, R., Demri, S., Lozes, E.: On the almighty wand. Technical report, LSV, ENS de Cachan (2008)","key":"30_CR5","DOI":"10.1007\/978-3-540-87531-4_24"},{"key":"30_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-540-87531-4_24","volume-title":"Computer Science Logic","author":"R. Brochenin","year":"2008","unstructured":"Brochenin, R., Demri, S., Lozes, \u00c9.: On the almighty wand (To appear). In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol.\u00a05213, pp. 323\u2013338. Springer, Heidelberg (2008)"},{"key":"30_CR7","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":"30_CR8","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1109\/TIME.2005.28","volume-title":"Proceedings of the 12th International Symposium on Temporal Representation and Reasoning (TIME 2005)","author":"S. Demri","year":"2005","unstructured":"Demri, S., Lazi\u0107, R., Nowak, D.: On the freeze quantifier in constraint LTL: Decidability and complexity. In: Proceedings of the 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), Burlington, Vermont, USA, pp. 113\u2013121. IEEE Computer Society Press, Los Alamitos (2005)"},{"key":"30_CR9","first-page":"226","volume-title":"PLDI 1997","author":"J. Jensen","year":"1997","unstructured":"Jensen, J., Jorgensen, M., Klarlund, N., Schwartzbach, M.: Automatic verification of pointer programs using monadic second-order logic. In: PLDI 1997, pp. 226\u2013236. ACM, New York (1997)"},{"key":"30_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-45099-3_15","volume-title":"Static Analysis","author":"T. Lev-Ami","year":"2000","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, pp. 280\u2013302. Springer, Heidelberg (2000)"},{"key":"30_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-540-71322-7_12","volume-title":"Program Analysis and Compilation, Theory and Practice","author":"A. Loginov","year":"2007","unstructured":"Loginov, A., Reps, T., Sagiv, M.: Refinement-based verification for possibly-cyclic lists. In: Reps, T., Sagiv, M., Bauer, J. (eds.) Wilhelm Festschrift. LNCS, vol.\u00a04444, pp. 247\u2013272. Springer, Heidelberg (2007)"},{"key":"30_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-540-69738-1_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H.H. Nguyen","year":"2007","unstructured":"Nguyen, H.H., David, C., Qin, S.C., Chin, W.-N.: Automated verification of shape and size properties via separation logic. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 251\u2013266. Springer, Heidelberg (2007)"},{"key":"30_CR13","first-page":"1","volume":"41","author":"M. Rabin","year":"1969","unstructured":"Rabin, M.: Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society\u00a041, 1\u201335 (1969)","journal-title":"Transactions of the American Mathematical Society"},{"key":"30_CR14","first-page":"55","volume-title":"LICS 2002","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS 2002, pp. 55\u201374. IEEE, Los Alamitos (2002)"},{"key":"30_CR15","first-page":"572","volume":"70","author":"B.A. Trakhtenbrot","year":"1950","unstructured":"Trakhtenbrot, B.A.: The impossibility of an algorithm for the decision problem for finite models. Dokl. Akad. Nauk SSSR\u00a070, 572\u2013596 (1950); English translation in: AMS Transl. Ser. 2,\u00a023(1063), 1\u20136","journal-title":"Dokl. Akad. Nauk SSSR"},{"key":"30_CR16","series-title":"Lecture Notes in Computer Science","first-page":"94","volume-title":"Foundations of Software Science and Computational Structures","author":"G. Yorsh","year":"2005","unstructured":"Yorsh, G., Rabinovich, A.M., Sagiv, M., Meyer, A., Bouajjani, A.: A logic of reachable patterns in linked data structures. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol.\u00a03441, pp. 94\u2013110. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computational Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-00596-1_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,8]],"date-time":"2025-02-08T18:24:29Z","timestamp":1739039069000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-00596-1_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642005954","9783642005961"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-00596-1_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}