{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:28:40Z","timestamp":1725542920888},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540377566"},{"type":"electronic","value":"9783540377580"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11823230_5","type":"book-chapter","created":{"date-parts":[[2006,8,17]],"date-time":"2006-08-17T13:46:30Z","timestamp":1155822390000},"page":"52-70","source":"Crossref","is-referenced-by-count":50,"title":["Abstract Regular Tree Model Checking of Complex Dynamic Data Structures"],"prefix":"10.1007","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Habermehl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adam","family":"Rogalewicz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom\u00e1\u0161","family":"Vojnar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/3-540-45694-5_9","volume-title":"CONCUR 2002 - Concurrency Theory","author":"P.A. Abdulla","year":"2002","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J.: Regular Model Checking Made Simple and Efficient. In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, p. 116. Springer, Heidelberg (2002)"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1007\/3-540-45657-0_47","volume-title":"Computer Aided Verification","author":"P.A. Abdulla","year":"2002","unstructured":"Abdulla, P.A., Jonsson, B., Mahata, P., d\u2019Orso, J.: Regular Tree Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 555. Springer, Heidelberg (2002)"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-540-31980-1_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P.A. Abdulla","year":"2005","unstructured":"Abdulla, P.A., Legay, A., d\u2019Orso, J., Rezine, A.: Simulation-Based Iteration of Tree Transducers. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 30\u201344. Springer, Heidelberg (2005)"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-540-30579-8_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"I. Balaban","year":"2005","unstructured":"Balaban, I., Pnueli, A., Zuck, L.D.: Shape Analysis by Predicate Abstraction. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 164\u2013180. Springer, Heidelberg (2005)"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Automata Implementation","author":"M. Biehl","year":"1997","unstructured":"Biehl, M., Klarlund, N., Rauhe, T.: Algorithms for Guided Tree Automata. In: Raymond, D.R., Yu, S., Wood, D. (eds.) WIA 1996. LNCS, vol.\u00a01260. Springer, Heidelberg (1997)"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-45069-6_24","volume-title":"Computer Aided Verification","author":"B. Boigelot","year":"2003","unstructured":"Boigelot, B., Legay, A., Wolper, P.: Iterating Transducers in the Large. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 223\u2013235. Springer, Heidelberg (2003)"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with Lists are Counter Automata. Technical Report TR-2006-3, Verimag, UJF\/CNRS\/INPG, Grenoble (2006)","DOI":"10.1007\/11817963_47"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/978-3-540-31980-1_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Bouajjani","year":"2005","unstructured":"Bouajjani, A., Habermehl, P., Moro, P., Vojnar, T.: Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 13\u201329. Springer, Heidelberg (2005)"},{"key":"5_CR9","first-page":"37","volume":"149","author":"A. Bouajjani","year":"2006","unstructured":"Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract Regular Tree Model Checking. ENTCS\u00a0149, 37\u201348 (2006); A preliminary version was presented at Infinity 2005","journal-title":"ENTCS"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract Regular Tree Model Checking of Complex Dynamic Data Structures (2006), Full version available on: http:\/\/www.fit.vutbr.cz\/~vojnar\/pubs.php","DOI":"10.1007\/11823230_5"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-540-27813-9_29","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2004","unstructured":"Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract Regular Model Checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 372\u2013386. Springer, Heidelberg (2004)"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_31","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2000","unstructured":"Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular Model Checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855. Springer, Heidelberg (2000)"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1007\/3-540-45657-0_46","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2002","unstructured":"Bouajjani, A., Touili, T.: Extrapolating Tree Transformations. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 539. Springer, Heidelberg (2002)"},{"key":"5_CR14","volume-title":"Proc. of PEPM 2003","author":"M. Bozga","year":"2003","unstructured":"Bozga, M., Iosif, R., Lakhnech, Y.: Storeless Semantics and Alias Logic. In: Proc. of PEPM 2003. ACM Press, New York (2003)"},{"key":"5_CR15","first-page":"113","volume":"145","author":"M. \u010ce\u0161ka","year":"2006","unstructured":"\u010ce\u0161ka, M., Erlebach, P., Vojnar, T.: Pattern-Based Verification of Programs with Extended Linear Linked Data Structures. ENTCS\u00a0145, 113\u2013130 (2006); A preliminary version was presented at AVOCS 2005","journal-title":"ENTCS"},{"key":"5_CR16","unstructured":"Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree Automata Techniques and Applications (2005), http:\/\/www.grappa.univ-lille3.fr\/tata"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/11691372_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.V. Deshmukh","year":"2006","unstructured":"Deshmukh, J.V., Emerson, E.A., Gupta, P.: Automatic Verification of Parameterized Data Structures. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 27\u201341. Springer, Heidelberg (2006)"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11691372_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Distefano","year":"2006","unstructured":"Distefano, D., O\u2019Hearn, P.W., Yang, H.: A Local Shape Analysis Based on Separation Logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 287\u2013302. Springer, Heidelberg (2006)"},{"key":"5_CR19","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/BF01704020","volume":"9","author":"J. Engelfriet","year":"1975","unstructured":"Engelfriet, J.: Bottom-up and Top-down Tree Transformations\u2014A Comparison. Mathematical System Theory\u00a09, 198\u2013231 (1975)","journal-title":"Mathematical System Theory"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/11691372_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Habermehl","year":"2006","unstructured":"Habermehl, P., Iosif, R., Vojnar, T.: Automata-Based Verification of Programs with Tree Updates. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 350\u2013364. Springer, Heidelberg (2006)"},{"key":"5_CR21","first-page":"21","volume":"138","author":"P. Habermehl","year":"2005","unstructured":"Habermehl, P., Vojnar, T.: Regular Model Checking Using Inference of Regular Languages. ENTCS\u00a0138, 21\u201336 (2005); A preliminary version was presented at Infinity 2004","journal-title":"ENTCS"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"Y. Kesten","year":"1997","unstructured":"Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic Model Checking with Rich Assertional Languages. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254. Springer, Heidelberg (1997)"},{"key":"5_CR23","unstructured":"Klarlund, N., M\u00f8ller, A.: MONA Version 1.4 User Manual, BRICS, Department of Computer Science, University of Aarhus, Denmark (2001)"},{"key":"5_CR24","volume-title":"Proc. of POPL 1993","author":"N. Klarlund","year":"1993","unstructured":"Klarlund, N., Schwartzbach, M.I.: Graph Types. In: Proc. of POPL 1993. ACM Press, New York (1993)"},{"key":"5_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-540-31987-0_10","volume-title":"Programming Languages and Systems","author":"O. Lee","year":"2005","unstructured":"Lee, O., Yang, H., Yi, K.: Automatic Verification of Pointer Programs Using Grammar-Based Shape Analysis. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 124\u2013140. Springer, Heidelberg (2005)"},{"key":"5_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/11513988_50","volume-title":"Computer Aided Verification","author":"A. Loginov","year":"2005","unstructured":"Loginov, A., Reps, T., Sagiv, M.: Abstraction Refinement via Inductive Learning. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 519\u2013533. Springer, Heidelberg (2005)"},{"key":"5_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-540-30579-8_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R. Manevich","year":"2005","unstructured":"Manevich, R., Yahav, E., Ramalingam, G., Sagiv, M.: Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 181\u2013198. Springer, Heidelberg (2005)"},{"key":"5_CR28","volume-title":"Proc. of PLDI 2001","author":"A. M\u00f8ller","year":"2001","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The Pointer Assertion Logic Engine. In: Proc. of PLDI 2001. ACM Press, New York (2001); also in SIGPLAN Notices 36(5), 2001"},{"key":"5_CR29","doi-asserted-by":"crossref","unstructured":"Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric Shape Analysis via 3-valued Logic. TOPLAS\u00a024(3) (2002)","DOI":"10.1145\/514188.514190"},{"key":"5_CR30","unstructured":"Shahar, E., Pnueli, A.: Acceleration in Verification of Parameterized Tree Networks. Technical Report MCS02-12, Faculty of Mathematics and Computer Science, The Weizmann Institute of Science, Rehovot, Israel (2002)"},{"key":"5_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-540-31980-1_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Vardhan","year":"2005","unstructured":"Vardhan, A., Sen, K., Viswanathan, M., Agha, G.A.: Using Language Inference to Verify Omega-Regular Properties. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 45\u201360. Springer, Heidelberg (2005)"},{"key":"5_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/3-540-45789-5_8","volume-title":"Static Analysis","author":"T. Yavuz-Kahveci","year":"2002","unstructured":"Yavuz-Kahveci, T., Bultan, T.: Automated Verification of Concurrent Linked Lists with Counters. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, p. 69. Springer, Heidelberg (2002)"},{"key":"5_CR33","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","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11823230_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:17:08Z","timestamp":1605644228000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11823230_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540377566","9783540377580"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/11823230_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}