{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,29]],"date-time":"2026-03-29T15:16:51Z","timestamp":1774797411414,"version":"3.50.1"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2009,11,21]],"date-time":"2009-11-21T00:00:00Z","timestamp":1258761600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2010,2]]},"DOI":"10.1007\/s00236-009-0108-5","type":"journal-article","created":{"date-parts":[[2009,11,20]],"date-time":"2009-11-20T22:21:52Z","timestamp":1258755712000},"page":"1-31","source":"Crossref","is-referenced-by-count":6,"title":["Automata-based verification of programs with tree updates"],"prefix":"10.1007","volume":"47","author":[{"given":"Peter","family":"Habermehl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Radu","family":"Iosif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom\u00e1\u0161","family":"Vojnar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,11,21]]},"reference":[{"key":"108_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proceedings of STOC\u201904. ACM Press (2004)","DOI":"10.1145\/1007352.1007390"},{"key":"108_CR2","unstructured":"Baldan, P., Corradini, A., Esparza, J., Heindel, T., K\u00f6nig, B., Kozioura, V.: Verifying red\u2013black trees. In: Proceedings of COSMICAH\u201905 (2005)"},{"key":"108_CR3","unstructured":"Barnett, M., Rustan, K., Leino, M., Schulte, W.: The Spec# programming system: an overview. In: Proceedings of CASSIS\u201904. Lectures Notes in Computer Science, vol. 3362. Springer (2004)"},{"key":"108_CR4","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model-checking. In: Proceedings of CONCUR\u201997. Lectures Notes in Computer Science, vol. 1243. Springer (1997)","DOI":"10.1007\/3-540-63141-0_10"},{"key":"108_CR5","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract regular tree model checking of complex dynamic data structures. In: Proceedings of the 13th International Symposium Static Analysis (SAS\u201906). Lecture Notes in Computer Science, vol. 4134, pp. 52\u201370. Springer (2006)","DOI":"10.1007\/11823230_5"},{"issue":"3","key":"108_CR6","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L. Burdy","year":"2005","unstructured":"Burdy L., Cheon Y., Cok D., Ernst M., Kiniry J., Leavens G.T., Rustan K., Leino M., Poll E.: An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transf. 7(3), 212\u2013232 (2005)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"108_CR7","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Gardner, P., Zarfaty, U.: Context logic and tree update. In: Proceedings of POPL\u201905. ACM Press (2005)","DOI":"10.1145\/1040305.1040328"},{"key":"108_CR8","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1016\/j.tcs.2004.09.036","volume":"331","author":"H. Comon-Lundh","year":"2005","unstructured":"Comon-Lundh H., Cortier V.: Tree automata with one memory, set constraints and cryptographic protocols. Theo. Comput. Sci. 331, 143\u2013214 (2005)","journal-title":"Theo. Comput. Sci."},{"key":"108_CR9","unstructured":"Comon-Lundh, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi. M.: Tree automata techniques and applications. Available at: http:\/\/www.grappa.univ-lille3.fr\/tata . Release Oct 1, 2002 (1997)"},{"key":"108_CR10","doi-asserted-by":"crossref","unstructured":"Comon-Lundh, H., Jaquemard, F., Perrin, N.: Tree automata with memory, visibility and structural constraints. In: Proceedings of FoSSaCS. Lecture Notes in Computer Science, vol. 4423. Springer (2007)","DOI":"10.1007\/978-3-540-71389-0_13"},{"key":"108_CR11","volume-title":"Introduction to Algorithms","author":"T.H. Cormen","year":"1990","unstructured":"Cormen T.H., Leiserson C.E., Rivest R.L.: Introduction to Algorithms. The MIT Press, Cambridge (1990)"},{"key":"108_CR12","unstructured":"Dal Zilio, S., Lugiez, D.: Multitrees automata, Presburger\u2019s constraints and tree logics. Technical Report 08-2002, LIF (2002)"},{"key":"108_CR13","doi-asserted-by":"crossref","unstructured":"Darga, P.T., Boyapati, C.: Efficient software model checking of data structure properties. In: Proceedings of OOPSLA\u201906. ACM Press (2006)","DOI":"10.1145\/1167473.1167504"},{"key":"108_CR14","first-page":"133","volume":"10","author":"D. Geidmanis","year":"1991","unstructured":"Geidmanis D.: Unsolvability of the emptiness problem for alternating 1-way multi-head and multi-tape finite automata over single-letter alphabet. Comput. Artif. Intell. 10, 133\u2013141 (1991)","journal-title":"Comput. Artif. Intell."},{"issue":"4","key":"108_CR15","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1023\/B:AUSE.0000038938.10589.b9","volume":"11","author":"S. Khurshid","year":"2004","unstructured":"Khurshid S., Marinov D.: TestEra: specification-based testing of Java programs using SAT. Automat. Softw. Eng. 11(4), 403\u2013434 (2004)","journal-title":"Automat. Softw. Eng."},{"key":"108_CR16","doi-asserted-by":"crossref","unstructured":"Manna, Z., Sipma, H.B., Zhang, T.: Verifying balanced trees. In: Proceedings of the Symposium on Logical Foundations of Computer Science (LFCS 2007). Lecture Notes in Computer Science, vol. 4514. Springer (2007)","DOI":"10.1007\/978-3-540-72734-7_26"},{"key":"108_CR17","doi-asserted-by":"crossref","unstructured":"Moeller, A., Schwartzbach, M.: The pointer assertion logic engine. In: Proceeedings of PLDI\u201901. ACM Press (2001)","DOI":"10.1145\/378795.378851"},{"key":"108_CR18","doi-asserted-by":"crossref","unstructured":"Nguyen, H.H., David, C., Qin, S., Chin, W.N.: Automated verification of shape and size properties via separation logic. In: Proceedings of VMCAI\u201907. Lecture Notes in Computer Science, vol. 4349. Springer (2007)","DOI":"10.1007\/978-3-540-69738-1_18"},{"key":"108_CR19","unstructured":"Parduhn, S.: Algorithm animation using shape analysis with special regard to binary trees. Technical Report, Universit\u00e4t des Saarlandes (2005)"},{"key":"108_CR20","doi-asserted-by":"crossref","unstructured":"Petersen, H.: Alternation in simple devices. In: Proceedings of ICALP\u201995. Lecture Notes in Computer Science, vol. 944. Springer (1995)","DOI":"10.1007\/3-540-60084-1_84"},{"key":"108_CR21","first-page":"1","volume":"141","author":"M.O. Rabin","year":"1969","unstructured":"Rabin M.O.: Decidability of second order theories and automata on infinite trees. Trans. Am. Math. Soc. 141, 1\u201335 (1969)","journal-title":"Trans. Am. Math. Soc."},{"key":"108_CR22","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of LICS\u201902. IEEE Computer Society Press (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"108_CR23","doi-asserted-by":"crossref","unstructured":"Rugina, R.: Quantitative shape analysis. In: Proceedings of SAS\u201904. Lecture Notes in Computer Sciences, vol. 3148. Springer (2004)","DOI":"10.1007\/978-3-540-27864-1_18"},{"issue":"3","key":"108_CR24","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"S. Sagiv","year":"2002","unstructured":"Sagiv S., Reps T.W., Wilhelm R.: Parametric shape analysis via 3-valued logic. TOPLAS 24(3), 217\u2013298 (2002)","journal-title":"TOPLAS"},{"key":"108_CR25","doi-asserted-by":"crossref","unstructured":"Seidl, H., Schwentick, T., Muscholl, A., Habermehl, P.: Counting in trees for free. In: Proceedings of ICALP\u201904. Lecture Notes in Computer Sciences, vol. 3142. Springer (2004)","DOI":"10.1007\/978-3-540-27836-8_94"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-009-0108-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-009-0108-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-009-0108-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,24]],"date-time":"2019-05-24T13:41:55Z","timestamp":1558705315000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-009-0108-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,11,21]]},"references-count":25,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2010,2]]}},"alternative-id":["108"],"URL":"https:\/\/doi.org\/10.1007\/s00236-009-0108-5","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,11,21]]}}}