{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:31:55Z","timestamp":1767929515370,"version":"3.49.0"},"publisher-location":"Cham","reference-count":82,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031572487","type":"print"},{"value":"9783031572494","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T00:00:00Z","timestamp":1712275200000},"content-version":"vor","delay-in-days":95,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p><jats:sc>Mata<\/jats:sc> is a well-engineered automata library written in C++ that offers a unique combination of speed and simplicity. It is meant to serve in applications such as string constraint solving and reasoning about regular expressions, and as a\u00a0reference implementation of automata algorithms. Besides basic algorithms for (non)deterministic automata, it implements a fast simulation reduction and antichain-based language inclusion checking. The simplicity allows a straightforward access to the low-level structures, making it relatively easy to extend and modify. Besides the C++ API, the library also implements a Python binding.<\/jats:p><jats:p>The library comes with a large benchmark of automata problems collected from relevant applications such as string constraint solving, regular model checking, and reasoning about regular expressions. We show that <jats:sc>Mata<\/jats:sc> is on this benchmark significantly faster than all libraries from a wide range of automata libraries we collected. Its usefulness in string constraint solving is demonstrated by the string solver <jats:sc>Z3-Noodler<\/jats:sc>, which is based on <jats:sc>Mata<\/jats:sc> and outperforms the state of the art in string constraint solving on many standard benchmarks.<\/jats:p>","DOI":"10.1007\/978-3-031-57249-4_7","type":"book-chapter","created":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T07:02:35Z","timestamp":1712214155000},"page":"130-151","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Mata: A Fast and Simple Finite Automata Library"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-5614-1592","authenticated-orcid":false,"given":"David","family":"Chocholat\u00fd","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0009-2596-9399","authenticated-orcid":false,"given":"Tom\u00e1\u0161","family":"Fiedor","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4375-7954","authenticated-orcid":false,"given":"Vojt\u011bch","family":"Havlena","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6957-1651","authenticated-orcid":false,"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2318-0940","authenticated-orcid":false,"given":"Martin","family":"Hru\u0161ka","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3038-5875","authenticated-orcid":false,"given":"Ond\u0159ej","family":"Leng\u00e1l","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7454-3751","authenticated-orcid":false,"given":"Juraj","family":"S\u00ed\u010d","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,4,5]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y., Diep, B.P., Hol\u00edk, L., Rezine, A., R\u00fcmmer, P.: Trau: SMT solver for string constraints. In: Proc. of FMCAD\u201918. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8602997"},{"key":"7_CR2","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y., Hol\u00edk, L., Rezine, A., R\u00fcmmer, P., Stenman, J.: String constraints for verification. In: Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. Lecture Notes in Computer Science, vol.\u00a08559, pp. 150\u2013166. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_10, https:\/\/doi.org\/10.1007\/978-3-319-08867-9_10","DOI":"10.1007\/978-3-319-08867-9_10 10.1007\/978-3-319-08867-9_10"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y.F., Hol\u00edk, L., Rezine, A., R\u00fcmmer, P., Stenman, J.: Norn: An SMT solver for string constraints. In: Computer Aided Verification. pp. 462\u2013469. Springer International Publishing, Cham (2015)","DOI":"10.1007\/978-3-319-21690-4_29"},{"key":"7_CR4","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Bouajjani, A., Hol\u00edk, L., Kaati, L., Vojnar, T.: Computing simulations over tree automata. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings. Lecture Notes in Computer Science, vol.\u00a04963, pp. 93\u2013108. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_8, https:\/\/doi.org\/10.1007\/978-3-540-78800-3_8","DOI":"10.1007\/978-3-540-78800-3_8 10.1007\/978-3-540-78800-3_8"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Chen, Y.F., Hol\u00edk, L., Mayr, R., Vojnar, T.: When simulation meets antichains. In: Proc. of TACAS\u201910. LNCS, vol.\u00a06015. Springer (2010)","DOI":"10.1007\/978-3-642-12002-2_14"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., Saksena, M.: A survey of regular model checking. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004 - Concurrency Theory. pp. 35\u201348. Springer Berlin Heidelberg, Berlin, Heidelberg (2004)","DOI":"10.1007\/978-3-540-28644-8_3"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Almeida, A., Almeida, M., Alves, J., Moreira, N., Reis, R.: Fado and guitar: Tools for automata manipulation and visualization. In: Maneth, S. (ed.) Implementation and Application of Automata. pp. 65\u201374. Springer Berlin Heidelberg, Berlin, Heidelberg (2009)","DOI":"10.1007\/978-3-642-02979-0_10"},{"key":"7_CR8","unstructured":"authors, A.: Amaya (2023), https:\/\/github.com\/MichalHe\/amaya"},{"key":"7_CR9","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). http:\/\/www.SMT-LIB.org (2016)"},{"key":"7_CR10","doi-asserted-by":"publisher","unstructured":"Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J.D., Nowotka, D., Ganesh, V.: An SMT solver for regular expressions and linear arithmetic over string length. In: Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12760, pp. 289\u2013312. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_14, https:\/\/doi.org\/10.1007\/978-3-030-81688-9_14","DOI":"10.1007\/978-3-030-81688-9_14 10.1007\/978-3-030-81688-9_14"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Blahoudek, F., Chen, Y.F., Chocholat\u00fd, D., Havlena, V., Hol\u00edk, L., Leng\u00e1l, O., S\u00ed\u010d, J.: Word equations in synergy with regular constraints. In: Proc. of FM\u201923. Springer (2023)","DOI":"10.1007\/978-3-031-27481-7_23"},{"key":"7_CR12","doi-asserted-by":"publisher","unstructured":"Boigelot, B., Latour, L.: Counting the solutions of Presburger equations without enumerating them. Theoretical Computer Science 313(1), 17\u201329 (2004). https:\/\/doi.org\/10.1016\/j.tcs.2003.10.002, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0304397503005322, implementation and Application of Automata","DOI":"10.1016\/j.tcs.2003.10.002"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Legay, A., Wolper, P.: Iterating transducers in the large. In: Hunt, W.A., Somenzi, F. (eds.) Computer Aided Verification. pp. 223\u2013235. Springer Berlin Heidelberg, Berlin, Heidelberg (2003)","DOI":"10.1007\/978-3-540-45069-6_24"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Bonchi, F., Pous, D.: Checking NFA equivalence with bisimulations up to congruence. In: Proc. of POPL\u201913. ACM (2013)","DOI":"10.1145\/2429069.2429124"},{"key":"7_CR15","unstructured":"Bouajjani, A., Habermehl, P., Hol\u00edk, L., Touili, T., Vojnar, T.: Antichain-based universality and inclusion testing over nondeterministic finite tree automata. In: Proc. of CIAA\u201908. Springer (2008)"},{"key":"7_CR16","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regular model checking. In: Alur, R., Peled, D.A. (eds.) Computer Aided Verification, 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings. Lecture Notes in Computer Science, vol.\u00a03114, pp. 372\u2013386. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_29, https:\/\/doi.org\/10.1007\/978-3-540-27813-9_29","DOI":"10.1007\/978-3-540-27813-9_29 10.1007\/978-3-540-27813-9_29"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Boudet, A., Comon, H.: Diophantine equations, Presburger arithmetic and finite automata. In: Kirchner, H. (ed.) Trees in Algebra and Programming \u2014 CAAP \u201996. pp. 30\u201343. Springer Berlin Heidelberg, Berlin, Heidelberg (1996)","DOI":"10.1007\/3-540-61064-2_27"},{"key":"7_CR18","doi-asserted-by":"publisher","unstructured":"Briggs, P., Torczon, L.: An efficient representation for sparse sets. ACM Lett. Program. Lang. Syst. 2(1\u20134), 59\u201369 (mar 1993). https:\/\/doi.org\/10.1145\/176454.176484, https:\/\/doi.org\/10.1145\/176454.176484","DOI":"10.1145\/176454.176484 10.1145\/176454.176484"},{"key":"7_CR19","unstructured":"Brzozowski, J.A.: Canonical regular expressions and minimal state graphs for definite events. In: Proc. of Symposium on Mathematical Theory of Automata (1962)"},{"key":"7_CR20","doi-asserted-by":"publisher","unstructured":"B\u00fcchi, J.R.: Weak Second-Order Arithmetic and Finite Automata, pp. 398\u2013424. Springer New York, New York, NY (1990). https:\/\/doi.org\/10.1007\/978-1-4613-8928-6_22, https:\/\/doi.org\/10.1007\/978-1-4613-8928-6_22","DOI":"10.1007\/978-1-4613-8928-6_22 10.1007\/978-1-4613-8928-6_22"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"C\u00e9c\u00e9, G.: Foundation for a series of efficient simulation algorithms. In: Proc. of LICS\u201917. IEEE (2017)","DOI":"10.1109\/LICS.2017.8005069"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Chen, T., Chen, Y., Hague, M., Lin, A.W., Wu, Z.: What is decidable about string constraints with the replaceall function. Proc. of POPL\u201918 (2018)","DOI":"10.1145\/3158091"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Chen, T., Hague, M., Lin, A.W., R\u00fcmmer, P., Wu, Z.: Decision procedures for path feasibility of string-manipulating programs with complex operations. Proc. of POPL\u201919 (2019)","DOI":"10.1145\/3290362"},{"key":"7_CR24","doi-asserted-by":"publisher","unstructured":"Chen, Y.F., Chocholat\u00fd, D., Havlena, V., Hol\u00edk, L., Leng\u00e1l, O., S\u00ed\u010d, J.: Solving string constraints with lengths by stabilization. Proc. ACM Program. Lang. 7(OOPSLA2) (oct 2023). https:\/\/doi.org\/10.1145\/3622872","DOI":"10.1145\/3622872"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Chen, Y.F., Chocholat\u00fd, D., Havlena, V., Hol\u00edk, L., Leng\u00e1l, O., S\u00ed\u010d, J.: Z3-noodler: An automata-based string solver. In: Proc. of TACAS\u201924. LNCS, Springer (2024)","DOI":"10.1007\/978-3-031-57246-3_2"},{"key":"7_CR26","doi-asserted-by":"publisher","unstructured":"Chen, Y., Hong, C., Lin, A.W., R\u00fcmmer, P.: Learning to prove safety over parameterised concurrent systems. In: Stewart, D., Weissenbacher, G. (eds.) 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, October 2-6, 2017. pp. 76\u201383. IEEE (2017). https:\/\/doi.org\/10.23919\/FMCAD.2017.8102244, https:\/\/doi.org\/10.23919\/FMCAD.2017.8102244","DOI":"10.23919\/FMCAD.2017.8102244 10.23919\/FMCAD.2017.8102244"},{"key":"7_CR27","doi-asserted-by":"publisher","unstructured":"Chocholat\u00fd, D., Fiedor, T., Havlena, V., Hol\u00edk, L., Hru\u0161ka, M., Leng\u00e1l, O., S\u00ed\u010d, J.: A replication package for reproducing the results of paper \u201cMata: A fast and simple finite automata library\u201d (Oct 2023). https:\/\/doi.org\/10.5281\/zenodo.10044515, https:\/\/doi.org\/10.5281\/zenodo.10044515","DOI":"10.5281\/zenodo.10044515 10.5281\/zenodo.10044515"},{"key":"7_CR28","unstructured":"Cox, A., Leasure, J.: Model checking regular language constraints. CoRR abs\/1708.09073 (2017)"},{"key":"7_CR29","unstructured":"D\u2019Antoni, L.: A symbolic automata library, https:\/\/github.com\/lorisdanto\/symbolicautomata"},{"key":"7_CR30","doi-asserted-by":"crossref","unstructured":"D\u2019Antoni, L., Kincaid, Z., Wang, F.: A symbolic decision procedure for symbolic alternating finite automata. Electronic Notes in Theoretical Computer Science 336 (2018)","DOI":"10.1016\/j.entcs.2018.03.017"},{"key":"7_CR31","doi-asserted-by":"crossref","unstructured":"D\u2019Antoni, L., Veanes, M.: Minimization of symbolic automata. In: Proc. of POPL\u201914. ACM (2014)","DOI":"10.1145\/2535838.2535849"},{"key":"7_CR32","doi-asserted-by":"crossref","unstructured":"D\u2019Antoni, L., Veanes, M.: Minimization of symbolic tree automata. In: Proc. of LICS\u201916. ACM (2016)","DOI":"10.1145\/2933575.2933578"},{"key":"7_CR33","doi-asserted-by":"crossref","unstructured":"D\u2019Antoni, L., Veanes, M.: The power of symbolic automata and transducers. In: Majumdar, R., Kun\u010dak, V. (eds.) Computer Aided Verification. pp. 47\u201367. Springer International Publishing, Cham (2017)","DOI":"10.1007\/978-3-319-63387-9_3"},{"key":"7_CR34","doi-asserted-by":"crossref","unstructured":"De\u00a0Wulf, M., Doyen, L., Maquet, N., Raskin, J.F.: Alaska. In: Proc. of ATVA\u201908. Springer (2008)","DOI":"10.1007\/978-3-540-88387-6_21"},{"key":"7_CR35","doi-asserted-by":"crossref","unstructured":"Doyen, L., Raskin, J.: Antichain algorithms for finite automata. In: Proc. of TACAS\u201910. LNCS, Springer (2010)","DOI":"10.1007\/978-3-642-12002-2_2"},{"key":"7_CR36","doi-asserted-by":"crossref","unstructured":"Duret-Lutz, A., Renault, E., Colange, M., Renkin, F., Gbaguidi\u00a0Aisse, A., Schlehuber-Caissier, P., Medioni, T., Martin, A., Dubois, J., Gillard, C., Lauko, H.: From Spot 2.0 to Spot 2.10: What\u2019s new? In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification. pp. 174\u2013187. Springer International Publishing, Cham (2022)","DOI":"10.1007\/978-3-031-13188-2_9"},{"key":"7_CR37","unstructured":"Evans, C.: Automata (2023), https:\/\/github.com\/caleb531\/automata"},{"key":"7_CR38","doi-asserted-by":"publisher","unstructured":"Fiedor, T., Hol\u00edk, L., Hruska, M., Rogalewicz, A., S\u00edc, J., Vargov\u010d\u00edk, P.: Reasoning about regular properties: A comparative study. In: Pientka, B., Tinelli, C. (eds.) Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings. Lecture Notes in Computer Science, vol. 14132, pp. 286\u2013306. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_17, https:\/\/doi.org\/10.1007\/978-3-031-38499-8_17","DOI":"10.1007\/978-3-031-38499-8_17 10.1007\/978-3-031-38499-8_17"},{"key":"7_CR39","doi-asserted-by":"crossref","unstructured":"Fu, C., Deng, Y., Jansen, D.N., Zhang, L.: On equivalence checking of nondeterministic finite automata. In: Proc. of SETTA\u201917. LNCS, Springer (2017)","DOI":"10.1007\/978-3-319-69483-2_13"},{"key":"7_CR40","doi-asserted-by":"crossref","unstructured":"Gange, G., Navas, J.A., Stuckey, P.J., S\u00f8ndergaard, H., Schachte, P.: Unbounded model-checking with interpolation for regular language constraints. In: Proc. of TACAS\u201913. LNCS, Springer (2013)","DOI":"10.1007\/978-3-642-36742-7_20"},{"key":"7_CR41","unstructured":"Google: Re2. https:\/\/github.com\/google\/re2"},{"key":"7_CR42","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification. pp. 36\u201352. Springer Berlin Heidelberg, Berlin, Heidelberg (2013)","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"7_CR43","doi-asserted-by":"crossref","unstructured":"Henriksen, J.G., Jensen, J.L., J\u00f8rgensen, M.E., Klarlund, N., Paige, R., Rauhe, T., Sandholm, A.: Mona: Monadic second-order logic in practice. In: Proc. of TACAS \u201995. LNCS, vol.\u00a01019. Springer (1995)","DOI":"10.7146\/brics.v2i21.19923"},{"key":"7_CR44","unstructured":"Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: Proc. of FOCS. IEEE (1995)"},{"key":"7_CR45","doi-asserted-by":"crossref","unstructured":"Hol\u00edk, L., Jank\u016f, P., Lin, A.W., R\u00fcmmer, P., Vojnar, T.: String constraints with concatenation and transducers solved efficiently. Proc. of POPL\u201918 2 (2018)","DOI":"10.1145\/3158092"},{"key":"7_CR46","doi-asserted-by":"crossref","unstructured":"Hol\u00edk, L., Leng\u00e1l, O., S\u00ed\u010d, J., Veanes, M., Vojnar, T.: Simulation algorithms for symbolic automata. In: Lahiri, S.K., Wang, C. (eds.) Proc. of ATVA\u201918. Springer (2018)","DOI":"10.1007\/978-3-030-01090-4_7"},{"key":"7_CR47","doi-asserted-by":"crossref","unstructured":"Hol\u00edk, L., Leng\u00e1l, O., \u0160im\u00e1\u010dek, J., Vojnar, T.: Efficient inclusion checking on explicit and semi-symbolic tree automata. In: Proc. of ATVA\u201911. LNCS, Springer (2011)","DOI":"10.1007\/978-3-642-24372-1_18"},{"key":"7_CR48","unstructured":"Hol\u00edk, L., \u0160im\u00e1\u010dek, J.: Optimizing an LTS-simulation algorithm. Computing and Informatics 29(6+), 1337\u20131348 (2010), https:\/\/arxiv.org\/abs\/2307.04235"},{"key":"7_CR49","doi-asserted-by":"crossref","unstructured":"Hooimeijer, P., Weimer, W.: A decision procedure for subset constraints over regular languages. In: PLDI\u201909. ACM (2009)","DOI":"10.1145\/1542476.1542498"},{"key":"7_CR50","doi-asserted-by":"crossref","unstructured":"Hopcroft, J.E.: An n log n algorithm for minimizing states in a finite automaton. Tech. rep., Stanford University, Stanford, CA, USA (1971)","DOI":"10.1016\/B978-0-12-417750-5.50022-1"},{"key":"7_CR51","doi-asserted-by":"crossref","unstructured":"Huffman, D.: The synthesis of sequential switching circuits. Journal of the Franklin Institute 257(3) (1954)","DOI":"10.1016\/0016-0032(54)90574-8"},{"key":"7_CR52","doi-asserted-by":"crossref","unstructured":"Ilie, L., Navarro, G., Yu, S.: On NFA reductions. In: Theory Is Forever: Essays Dedicated to Arto Salomaa on the Occasion of His 70th Birthday. Springer (2004)","DOI":"10.1007\/978-3-540-27812-2_11"},{"key":"7_CR53","unstructured":"Isberner, M., Howar, F., Steffen, B.: AutomataLib, https:\/\/learnlib.de\/projects\/automatalib\/"},{"key":"7_CR54","doi-asserted-by":"crossref","unstructured":"Isberner, M., Howar, F., Steffen, B.: The open-source learnlib. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) Computer Aided Verification. pp. 487\u2013495. Springer International Publishing, Cham (2015)","DOI":"10.1007\/978-3-319-21690-4_32"},{"key":"7_CR55","doi-asserted-by":"publisher","unstructured":"Kelb, P., Margaria, T., Mendler, M., Gsottberger, C.: MOSEL: A sound and efficient tool for M2L(Str). In: Grumberg, O. (ed.) Computer Aided Verification, 9th International Conference, CAV \u201997, Haifa, Israel, June 22-25, 1997, Proceedings. Lecture Notes in Computer Science, vol.\u00a01254, pp. 448\u2013451. Springer (1997). https:\/\/doi.org\/10.1007\/3-540-63166-6_45, https:\/\/doi.org\/10.1007\/3-540-63166-6_45","DOI":"10.1007\/3-540-63166-6_45 10.1007\/3-540-63166-6_45"},{"key":"7_CR56","unstructured":"Klaedtke, F.C.: Automata-based decision procedures for weak arithmetics. Ph.D. thesis, University of Freiburg, Freiburg im Breisgau, Germany (2004), http:\/\/freidok.ub.uni-freiburg.de\/volltexte\/1439\/index.html"},{"key":"7_CR57","doi-asserted-by":"crossref","unstructured":"K\u0159et\u00ednsk\u00fd, J., Meggendorfer, T., Sickert, S.: Owl: A library for $$\\omega $$-words, automata, and LTL. In: Lahiri, S.K., Wang, C. (eds.) Automated Technology for Verification and Analysis. pp. 543\u2013550. Springer International Publishing, Cham (2018)","DOI":"10.1007\/978-3-030-01090-4_34"},{"key":"7_CR58","doi-asserted-by":"crossref","unstructured":"Legay, A.: T(O)RMC: A tool for ($$\\omega $$)-regular model checking. In: Gupta, A., Malik, S. (eds.) Computer Aided Verification. pp. 548\u2013551. Springer Berlin Heidelberg, Berlin, Heidelberg (2008)","DOI":"10.1007\/978-3-540-70545-1_52"},{"key":"7_CR59","doi-asserted-by":"crossref","unstructured":"Leng\u00e1l, O., \u0160im\u00e1\u010dek, J., Vojnar, T.: VATA: A library for efficient manipulation of non-deterministic tree automata. In: Proc. of TACAS\u201912. LNCS, vol.\u00a07214. Springer (2012)","DOI":"10.1007\/978-3-642-28756-5_7"},{"key":"7_CR60","unstructured":"Lombardy, S., Marsault, V., Sakarovitch, J.: Awali, a library for weighted automata and transducers (version 2.0) (2021), software available at http:\/\/vaucanson-project.org\/Awali\/2.0\/"},{"key":"7_CR61","unstructured":"Lutterkort, D.: libfa, https:\/\/augeas.net\/libfa\/"},{"key":"7_CR62","doi-asserted-by":"crossref","unstructured":"Moore, E.F.: Gedanken-experiments on sequential machines. In: Automata Studies. Volume 34. Princeton University Press, Princeton (1956)","DOI":"10.1515\/9781400882618-006"},{"key":"7_CR63","unstructured":"M\u00f8ller, A., et\u00a0al.: Brics automata library, https:\/\/www.brics.dk\/automaton\/"},{"key":"7_CR64","doi-asserted-by":"crossref","unstructured":"Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM Journal on Computing 16(6) (1987)","DOI":"10.1137\/0216062"},{"key":"7_CR65","doi-asserted-by":"crossref","unstructured":"Ranzato, F., Tapparo, F.: An efficient simulation algorithm based on abstract interpretation. Information and Computation 208, 1\u201322 (2010)","DOI":"10.1016\/j.ic.2009.06.002"},{"key":"7_CR66","unstructured":"RegExLib.com: The Internet\u2019s first Regular Expression Library. http:\/\/regexlib.com\/"},{"key":"7_CR67","unstructured":"SMT-LIB: https:\/\/clc-gitlab.cs.uiowa.edu:2443\/SMT-LIB-benchmarks\/QF_S (2023)"},{"key":"7_CR68","unstructured":"SMT-LIB: https:\/\/clc-gitlab.cs.uiowa.edu:2443\/SMT-LIB-benchmarks\/QF_SLIA (2023)"},{"key":"7_CR69","unstructured":"SMT-LIB: https:\/\/clc-gitlab.cs.uiowa.edu:2443\/SMT-LIB-benchmarks\/LIA (2023)"},{"key":"7_CR70","unstructured":"Somenzi, F.: CUDD: CU decision diagram package release 3.0.0 (2015)"},{"key":"7_CR71","doi-asserted-by":"crossref","unstructured":"Stanford, C., Veanes, M., Bj\u00f8rner, N.S.: Symbolic boolean derivatives for efficiently solving extended regular expression constraints. In: Proc. of PLDI\u201921. ACM (2021)","DOI":"10.1145\/3453483.3454066"},{"key":"7_CR72","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0. Journal of Automated Reasoning 59(4), 483\u2013502 (2017)","DOI":"10.1007\/s10817-017-9407-7"},{"key":"7_CR73","doi-asserted-by":"publisher","unstructured":"Tarjan, R.E.: Depth-first search and linear graph algorithms (working paper). In: 12th Annual Symposium on Switching and Automata Theory, East Lansing, Michigan, USA, October 13-15, 1971. pp. 114\u2013121. IEEE Computer Society (1971). https:\/\/doi.org\/10.1109\/SWAT.1971.10, https:\/\/doi.org\/10.1109\/SWAT.1971.10","DOI":"10.1109\/SWAT.1971.10 10.1109\/SWAT.1971.10"},{"key":"7_CR74","doi-asserted-by":"publisher","unstructured":"Tozawa, A., Hagiya, M.: XML schema containment checking based on semi-implicit techniques. In: Ibarra, O.H., Dang, Z. (eds.) Implementation and Application of Automata, 8th International Conference, CIAA 2003, Santa Barbara, California, USA, July 16-18, 2003, Proceedings. Lecture Notes in Computer Science, vol.\u00a02759, pp. 213\u2013225. Springer (2003). https:\/\/doi.org\/10.1007\/3-540-45089-0_20, https:\/\/doi.org\/10.1007\/3-540-45089-0_20","DOI":"10.1007\/3-540-45089-0_20 10.1007\/3-540-45089-0_20"},{"key":"7_CR75","doi-asserted-by":"crossref","unstructured":"Tsay, Y.K., Chen, Y.F., Tsai, M.H., Wu, K.N., Chan, W.C.: Goal: A graphical tool for manipulating b\u00fcchi automata and temporal formulae. In: Grumberg, O., Huth, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 466\u2013471. Springer Berlin Heidelberg, Berlin, Heidelberg (2007)","DOI":"10.1007\/978-3-540-71209-1_35"},{"key":"7_CR76","doi-asserted-by":"crossref","unstructured":"Valmari, A.: Simple bisimilarity minimization in O(m log n) time. Fundamenta Informaticae 105(3) (2010)","DOI":"10.3233\/FI-2010-369"},{"key":"7_CR77","unstructured":"Veanes, M.: A .NET automata library, https:\/\/github.com\/AutomataDotNet\/Automata"},{"key":"7_CR78","doi-asserted-by":"crossref","unstructured":"Veanes, M., de\u00a0Halleux, P., Tillmann, N.: Rex: Symbolic regular expression explorer. In: Proc. of ICST\u201910. IEEE (2010)","DOI":"10.1109\/ICST.2010.15"},{"key":"7_CR79","doi-asserted-by":"crossref","unstructured":"Wang, H., Tsai, T., Lin, C., Yu, F., Jiang, J.R.: String analysis via automata manipulation with logic circuit representation. In: Proc. of CAV\u201916. LNCS, vol.\u00a09779. Springer (2016)","DOI":"10.1007\/978-3-319-41528-4_13"},{"key":"7_CR80","doi-asserted-by":"crossref","unstructured":"Wolper, P., Boigelot, B.: An automata-theoretic approach to Presburger arithmetic constraints (extended abstract). In: Mycroft, A. (ed.) Proc. of SAS\u201995. LNCS, vol.\u00a0983. Springer (1995)","DOI":"10.1007\/3-540-60360-3_30"},{"key":"7_CR81","doi-asserted-by":"crossref","unstructured":"Wolper, P., Boigelot, B.: Verifying systems with infinite but regular state spaces. In: Hu, A.J., Vardi, M.Y. (eds.) Computer Aided Verification. pp. 88\u201397. Springer Berlin Heidelberg, Berlin, Heidelberg (1998)","DOI":"10.1007\/BFb0028736"},{"key":"7_CR82","unstructured":"Wulf, M.D., Doyen, L., Henzinger, T.A., Raskin, J.: Antichains: A new algorithm for checking universality of finite automata. In: Proc. of CAV\u201906. LNCS, vol.\u00a04144. Springer (2006)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57249-4_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T07:07:20Z","timestamp":1712214440000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57249-4_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572487","9783031572494"],"references-count":82,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57249-4_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"5 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"53","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}