{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:03:06Z","timestamp":1776304986577,"version":"3.50.1"},"reference-count":60,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2011,7,20]],"date-time":"2011-07-20T00:00:00Z","timestamp":1311120000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2012,4]]},"DOI":"10.1007\/s10009-011-0205-y","type":"journal-article","created":{"date-parts":[[2011,7,19]],"date-time":"2011-07-19T11:32:11Z","timestamp":1311075131000},"page":"167-191","source":"Crossref","is-referenced-by-count":33,"title":["Abstract regular (tree) model checking"],"prefix":"10.1007","volume":"14","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","published-online":{"date-parts":[[2011,7,20]]},"reference":[{"key":"205_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Chen, Y.-F., Hol\u00edk, L., Mayr, R., Vojnar, T.: When simulation meets antichains (on Checking Language Inclusion of NFAs). In: Proceedings of TACAS\u201910. LNCS, vol. 6015. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-12002-2_14"},{"key":"205_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J., Saksena, M.: Regular model checking for MSO + LTL. In: Proceedings of CAV\u201904. LNCS, vol. 3114. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-27813-9_27"},{"key":"205_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J., Saksena, M.: Regular model checking for LTL(MSO). Special section on regular model checking. STTT (2010, this volume)","DOI":"10.1007\/s10009-011-0212-z"},{"key":"205_CR4","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., d\u2019Orso, J., Jonsson, B., Nilsson, M.: Regular model checking made simple and efficient. In: Proceedings of CONCUR\u201902. LNCS, vol. 2421. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45694-5_9"},{"key":"205_CR5","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., d\u2019Orso, J., Jonsson, B., Nilsson, M.: Algorithmic improvements in regular model checking. In: Proceedings of CAV\u201903. LNCS, vol. 2725. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-45069-6_25"},{"key":"205_CR6","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B., Mahata, P., d\u2019Orso, J.: Regular tree model checking. In: Proceedings of CAV\u201902. LNCS, vol. 2404. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45657-0_47"},{"key":"205_CR7","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Legay, A., d\u2019Orso, J., Rezine A.: Simulation-based iteration of tree transducers. In: Proceedings of TACAS\u201905. LNCS, vol. 3440. Springer, Berlin (2005)","DOI":"10.1007\/978-3-540-31980-1_3"},{"key":"205_CR8","doi-asserted-by":"crossref","unstructured":"Bensalem, S., Lakhnech, Y., Owre, S.: Computing abstractions of infinite state systems compositionally and automatically. In: Proceedings of CAV\u201998. LNCS, vol. 1427. Springer, Berlin (1998)","DOI":"10.1007\/BFb0028755"},{"key":"205_CR9","unstructured":"Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P., Wies, T., Yang, H.: Shape analysis for composite data structures. In: Proceedings of CAV\u201907. LNCS, vol. 4490. Springer, Berlin (2007)"},{"key":"205_CR10","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Legay, A., Wolper, P.: Iterating transducers in the large. In: Proceedings of CAV\u201903. LNCS, vol. 2725. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-45069-6_24"},{"key":"205_CR11","unstructured":"Bouajjani, A., Habermehl, P., Hol\u00edk, L., Touili, T., Vojnar, T.: Antichain-based universality and inclusion testing over nondeterministic finite tree automata. In: Proceedings of CIAA\u201908. LNCS, vol. 5148. Springer, Berlin (2008)"},{"key":"205_CR12","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Habermehl, P., Moro, P., Vojnar, T.: Verifying programs with dynamic 1-selector-linked structures in regular model checking. In: Proceedings of TACAS\u201905. LNCS, vol. 3440. Springer, Berlin (2005)","DOI":"10.1007\/978-3-540-31980-1_2"},{"key":"205_CR13","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract regular tree model checking. In: Proceedings of Infinity\u201905. ENTCS 149:37\u201348 (2006)","DOI":"10.1016\/j.entcs.2005.11.015"},{"key":"205_CR14","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 SAS\u201906. LNCS, vol. 4134. Springer, Berlin (2006)","DOI":"10.1007\/11823230_5"},{"key":"205_CR15","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regular model checking. In: Proceedings of CAV\u201904. LNCS, vol. 3114. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-27813-9_29"},{"key":"205_CR16","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Proceedings of CAV\u201900. LNCS, vol. 1855. Springer, Berlin (2000)","DOI":"10.1007\/10722167_31"},{"key":"205_CR17","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Legay, A., Wolper, P.: Handling liveness properties in (\u03c9-)regular model checking. In: Proceedings of Infinity\u201904. ENTCS 138:101\u2013115 (2005)","DOI":"10.1016\/j.entcs.2005.02.061"},{"key":"205_CR18","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Touili, T.: Extrapolating tree transformations. In: Proceedings of CAV\u201902. LNCS, vol. 2404. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45657-0_46"},{"key":"205_CR19","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Touili, T.: Widening techniques for regular tree model checking. Special section on regular model checking. STTT (2010, this volume)","DOI":"10.1007\/s10009-011-0208-8"},{"key":"205_CR20","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. In: Proceedings of POPL\u201909. ACM Press, New York (2009)","DOI":"10.1145\/1480881.1480917"},{"key":"205_CR21","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Proceedings of CAV\u201900. LNCS, vol. 1855. Springer, Berlin (2000)","DOI":"10.1007\/10722167_15"},{"key":"205_CR22","unstructured":"Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications. http:\/\/www.grappa.univ-lille3.fr\/tata (2005)"},{"key":"205_CR23","doi-asserted-by":"crossref","unstructured":"Dams, D., Lakhnech, Y., Steffen, M.: Iterating transducers. In: Proceedings of CAV\u201901. LNCS, vol. 2102. Springer, Berlin (2001)","DOI":"10.1007\/3-540-44585-4_27"},{"key":"205_CR24","doi-asserted-by":"crossref","unstructured":"Das, S., Dill, D.L.: Counter-example based predicate discovery in predicate abstraction. In: Proceedings of FMCAD\u201902 (2002)","DOI":"10.1007\/3-540-36126-X_2"},{"key":"205_CR25","doi-asserted-by":"crossref","unstructured":"Deshmukh, J.V., Emerson, E.A., Gupta, P.: Automatic verification of parameterized data structures. In: Proceedings of TACAS\u201906. LNCS, vol. 3920. Springer, Berlin (2006)","DOI":"10.1007\/11691372_2"},{"key":"205_CR26","doi-asserted-by":"crossref","unstructured":"Doyen, L., Raskin, J.-F.: Antichain algorithms for finite automata. In: Proceedings of TACAS\u201910. LNCS, vol. 6015. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-12002-2_2"},{"key":"205_CR27","doi-asserted-by":"crossref","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. Math. Syst. Theory 9, 198\u2013231 (1975)","journal-title":"Math. Syst. Theory"},{"key":"205_CR28","doi-asserted-by":"crossref","unstructured":"Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Proceedings of CAV\u201900. LNCS, vol. 1855. Springer, Berlin (2000)","DOI":"10.1007\/10722167_20"},{"key":"205_CR29","doi-asserted-by":"crossref","unstructured":"Fribourg, L., Olsen, H.: Reachability sets of parametrized rings as regular languages. In: Proceedings of Infinity\u201997, ENTCS 9 (1997)","DOI":"10.1016\/S1571-0661(05)80427-X"},{"key":"205_CR30","doi-asserted-by":"crossref","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Proceedings of CAV\u201997. LNCS, vol. 1254. Springer, Berlin (1997)","DOI":"10.1007\/3-540-63166-6_10"},{"key":"205_CR31","doi-asserted-by":"crossref","unstructured":"Guo, B., Vachharajani, N., August, D.I.: Shape analysis with inductive recursion synthesis. In: Proceedings of PLDI\u201907. ACM Press, New York (2007)","DOI":"10.1145\/1250734.1250764"},{"key":"205_CR32","doi-asserted-by":"crossref","unstructured":"Habermehl, P., Hol\u00edk, L., Rogalewicz, A., \u0160im\u00e1\u010dek, J., Vojnar, T.: Forest automata for verification of heap manipulation. In: Proceedings of CAV\u201911. LNCS, vol. 6806. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22110-1_34"},{"key":"205_CR33","doi-asserted-by":"crossref","unstructured":"Habermehl, P., Vojnar, T.: Regular model checking using inference of regular languages. In: Proceedings of Infinity\u201904. ENTCS 138:21\u201336 (2005)","DOI":"10.1016\/j.entcs.2005.01.044"},{"key":"205_CR34","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of POPL\u201902. ACM Press, New York (2002)","DOI":"10.1145\/503272.503279"},{"key":"205_CR35","doi-asserted-by":"crossref","unstructured":"Jonsson, B., Nilsson, M.: Transitive closures of regular relations for verifying infinite-state systems. In: Proceedings of TACAS\u201900. LNCS, vol. 1785. Springer, Berlin (2000)","DOI":"10.1007\/3-540-46419-0_16"},{"key":"205_CR36","doi-asserted-by":"crossref","unstructured":"Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. In: Proceedings of CAV\u201997. LNCS, vol. 1254. Springer, Berlin (1997)","DOI":"10.1007\/3-540-63166-6_41"},{"key":"205_CR37","unstructured":"Klarlund, N., M\u00f8ller, A.: MONA Version 1.4 User Manual, 2001. BRICS, Department of Computer Science, University of Aarhus, Denmark (2001)"},{"key":"205_CR38","doi-asserted-by":"crossref","unstructured":"Klarlund, N., Schwartzbach, M.I.: Graph types. In: Proceedings of POPL\u201993. ACM Press, New York (1993)","DOI":"10.1145\/158511.158628"},{"key":"205_CR39","doi-asserted-by":"crossref","unstructured":"Legay, A.: Extrapolating (Omega-)regular model checking. Special section on regular model checking. STTT (2010, this volume)","DOI":"10.1145\/1838552.1838554"},{"key":"205_CR40","doi-asserted-by":"crossref","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: Proceedings of PLDI\u201901. ACM Press, New York (2001)","DOI":"10.1145\/378795.378851"},{"key":"205_CR41","unstructured":"Nilsson, M.: Regular model checking. Licentiate Thesis, Uppsala University, Sweden (2000)"},{"key":"205_CR42","unstructured":"Nilsson, M.: Regular model checking. PhD thesis, Uppsala University (2005)"},{"key":"205_CR43","volume-title":"Infinite Words: Automata, Semigroups, Logic and Games","author":"D. Perrin","year":"2003","unstructured":"Perrin D., Pin J.-E.: Infinite Words: Automata, Semigroups, Logic and Games. Academic Press, New York (2003)"},{"key":"205_CR44","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Shahar, E.: Liveness and acceleration in parameterized verification. In: Proceedings of CAV 2000. LNCS, vol. 1855. Springer, Berlin (2000)","DOI":"10.1007\/10722167_26"},{"key":"205_CR45","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of LICS\u201902. IEEE CS Press (2002)"},{"key":"205_CR46","unstructured":"Rogalewicz, A.: Verification of programs with complex data structures. PhD thesis, FIT, Brno University of Technology (2005)"},{"issue":"3","key":"205_CR47","doi-asserted-by":"crossref","first-page":"1","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), 1\u201350 (2002)","journal-title":"TOPLAS"},{"key":"205_CR48","doi-asserted-by":"crossref","unstructured":"Saidi, H.: Model checking guided abstraction and analysis. In: Proceedings of SAS\u201900. LNCS, vol. 1824. Springer, Berlin (2000)","DOI":"10.1007\/978-3-540-45099-3_20"},{"key":"205_CR49","unstructured":"Schuppan, V., Biere, A.: Liveness checking as safety checking for infinite state spaces. In: Proceedings of Infinity\u201905 (2005)"},{"key":"205_CR50","unstructured":"Shahar, E.: Tools and techniques for verifying parameterized systems. PhD thesis, Weizmann Institute of Science, Rehovot, Israel (2001)"},{"key":"205_CR51","unstructured":"Shahar, E., Pnueli, A.: Acceleration in verification of parameterized tree networks. Technical Report MCS02-12, Weizmann Institute of Science, Rehovot, Israel (2002)"},{"key":"205_CR52","doi-asserted-by":"crossref","unstructured":"Touili, T.: Regular model checking using widening techniques. ENTCS 50 (2001)","DOI":"10.1016\/S1571-0661(04)00187-2"},{"key":"205_CR53","unstructured":"van Noord, G.: FSA6.2, 2004. http:\/\/odur.let.rug.nl\/~vannoord\/Fsa\/"},{"key":"205_CR54","doi-asserted-by":"crossref","unstructured":"Vardhan, A., Sen, K., Viswanathan, M., Agha, G.: Actively learning to verify safety for FIFO automata. In: Proceedings of FSTTCS\u201904. LNCS, vol. 3328. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-30538-5_41"},{"key":"205_CR55","doi-asserted-by":"crossref","unstructured":"Vardhan, A., Sen, K., Viswanathan, M., Agha, G.: Learning to verify safety properties. In: Proceedings of ICFEM\u201904. LNCS, vol. 3308. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-30482-1_26"},{"key":"205_CR56","doi-asserted-by":"crossref","unstructured":"Vardhan, A., Sen, K., Viswanathan, M., Agha, G.: Using language inference to verify omega-regular properties. In: Proceedings of TACAS\u201905. LNCS, vol. 3440. Springer, Berlin (2005)","DOI":"10.1007\/978-3-540-31980-1_4"},{"key":"205_CR57","doi-asserted-by":"crossref","unstructured":"Vardhan, A., Viswanathan, M.: Learning to verify branching time properties. In: Proceedings of ASE\u201905. IEEE\/ACM (2005)","DOI":"10.1145\/1101908.1101961"},{"key":"205_CR58","unstructured":"Vojnar, T.: Cut-offs and automata in formal verification of infinite-state systems. Habilitation thesis, FIT, Brno University of Technology, Czech Republic (2007)"},{"key":"205_CR59","doi-asserted-by":"crossref","unstructured":"Wolper, P., Boigelot, B.: Verifying systems with infinite but regular state spaces. In: Proceedings of CAV\u201998. LNCS, vol. 1427. Springer, Berlin (1998)","DOI":"10.1007\/BFb0028736"},{"key":"205_CR60","unstructured":"Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.W.: Scalable shape analysis for systems code. In: Proceedings of CAV\u201908. LNCS, vol. 5123. Springer, Berlin (2008)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0205-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-011-0205-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0205-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,28]],"date-time":"2021-11-28T09:44:37Z","timestamp":1638092677000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-011-0205-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,7,20]]},"references-count":60,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,4]]}},"alternative-id":["205"],"URL":"https:\/\/doi.org\/10.1007\/s10009-011-0205-y","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,7,20]]}}}