{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,18]],"date-time":"2025-10-18T10:30:26Z","timestamp":1760783426461,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642224379"},{"type":"electronic","value":"9783642224386"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-22438-6_36","type":"book-chapter","created":{"date-parts":[[2011,7,18]],"date-time":"2011-07-18T18:21:44Z","timestamp":1311013304000},"page":"476-491","source":"Crossref","is-referenced-by-count":22,"title":["An Efficient Decision Procedure for Imperative Tree Data Structures"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Wies","sequence":"first","affiliation":[]},{"given":"Marco","family":"Mu\u00f1iz","sequence":"additional","affiliation":[]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"36_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-540-69738-1_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"I. Balaban","year":"2007","unstructured":"Balaban, I., Pnueli, A., Zuck, L.D.: Shape analysis of single-parent heaps. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 91\u2013105. Springer, Heidelberg (2007)"},{"key":"36_CR2","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)"},{"key":"36_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Service Availability","author":"A. Bouajjani","year":"2006","unstructured":"Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract regular tree model checking of complex dynamic data structures. In: Penkler, D., Reitenspiess, M., Tam, F. (eds.) SAS 2006. LNCS, vol.\u00a04328, Springer, Heidelberg (2006)"},{"key":"36_CR4","volume-title":"Handbook of Automated Reasoning","author":"D. Calvanese","year":"2001","unstructured":"Calvanese, D., di Giacomo, G., Nardi, D., Lenzerini, M.: Reasoning in expressive description logics. In: Handbook of Automated Reasoning. Elsevier, Amsterdam (2001)"},{"key":"36_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-16242-8_14","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"W. Charatonik","year":"2010","unstructured":"Charatonik, W., Witkowski, P.: On the complexity of the bernays-sch\u00f6nfinkel class with datalog. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol.\u00a06397, pp. 187\u2013201. Springer, Heidelberg (2010)"},{"key":"36_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"doi-asserted-by":"crossref","unstructured":"Genev\u00e8s, P., Laya\u00efda, N., Schmitt, A.: Efficient static analysis of XML paths and types. In: ACM PLDI (2007)","key":"36_CR7","DOI":"10.1145\/1250734.1250773"},{"key":"36_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s00236-009-0108-5","volume":"47","author":"P. Habermehl","year":"2010","unstructured":"Habermehl, P., Iosif, R., Vojnar, T.: Automata-based verification of programs with tree updates. Acta Inf.\u00a047, 1\u201331 (2010)","journal-title":"Acta Inf."},{"key":"36_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-540-78800-3_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Ihlemann","year":"2008","unstructured":"Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On local reasoning in verification. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 265\u2013281. Springer, Heidelberg (2008)"},{"key":"36_CR10","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. M., Reps, T. W., 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)"},{"unstructured":"Klarlund, N., M\u00f8ller, A.: MONA Version 1.4 User Manual. BRICS Notes Series NS-01-1, Department of Computer Science, University of Aarhus (January 2001)","key":"36_CR11"},{"unstructured":"Kuncak, V.: Modular Data Structure Verification. PhD thesis, EECS Department, Massachusetts Institute of Technology (February 2007)","key":"36_CR12"},{"doi-asserted-by":"crossref","unstructured":"Lahiri, S., Qadeer, S.: Back to the future: revisiting precise program verification using SMT solvers. In: POPL (2008)","key":"36_CR13","DOI":"10.1145\/1328438.1328461"},{"key":"36_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/11532231_8","volume-title":"Automated Deduction \u2013 CADE-20","author":"T. Lev-Ami","year":"2005","unstructured":"Lev-Ami, T., Immerman, N., Reps, T., Sagiv, M., Srivastava, S., Yorsh, G.: Simulating reachability using first-order logic with applications to verification of linked data structures. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 99\u2013115. Springer, Heidelberg (2005)"},{"key":"36_CR15","first-page":"249","volume-title":"ACM Symposium on the Principles of Programming Languages (POPL 2010)","author":"A. Podelski","year":"2010","unstructured":"Podelski, A., Wies, T.: Counterexample-guided focus. In: ACM Symposium on the Principles of Programming Languages (POPL 2010), pp. 249\u2013260. ACM, New York (2010)"},{"key":"36_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/11532231_16","volume-title":"Automated Deduction \u2013 CADE-20","author":"V. Sofronie-Stokkermans","year":"2005","unstructured":"Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 219\u2013234. Springer, Heidelberg (2005)"},{"unstructured":"Wies, T.: Symbolic Shape Analysis. PhD thesis, University of Freiburg (2009)","key":"36_CR17"},{"doi-asserted-by":"crossref","unstructured":"Wies, T., Kuncak, V., Lam, P., Podelski, A., Rinard, M.: Field constraint analysis. In: Proc. Int. Conf. Verification, Model Checking, and Abstract Interpratation (2006)","key":"36_CR18","DOI":"10.1007\/11609773_11"},{"doi-asserted-by":"crossref","unstructured":"Wies, T., Mu\u00f1iz, M., Kuncak, V.: On an efficient decision procedure for imperative tree data structures. Technical Report IST-2011-0005, EPFL-REPORT-165193, IST Austria, EPFL (2011)","key":"36_CR19","DOI":"10.1007\/978-3-642-22438-6_36"},{"doi-asserted-by":"crossref","unstructured":"Yorsh, G., Rabinovich, A.M., Sagiv, M., Meyer, A., Bouajjani, A.: A logic of reachable patterns in linked data-structures. J. Log. Algebr. Program. (2007)","key":"36_CR20","DOI":"10.1007\/11690634_7"},{"doi-asserted-by":"crossref","unstructured":"Zee, K., Kuncak, V., Rinard, M.: Full functional verification of linked data structures. In: PLDI (2008)","key":"36_CR21","DOI":"10.1145\/1375581.1375624"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-23"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22438-6_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T20:08:10Z","timestamp":1558296490000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22438-6_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642224379","9783642224386"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22438-6_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}