{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:48:47Z","timestamp":1767926927032,"version":"3.49.0"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2021,4,26]],"date-time":"2021-04-26T00:00:00Z","timestamp":1619395200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"National Science Foundation","award":["1750965"],"award-info":[{"award-number":["1750965"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Commun. ACM"],"published-print":{"date-parts":[[2021,5]]},"abstract":"<jats:p>Symbolic automata better balances how automata are implemented in practice.<\/jats:p>","DOI":"10.1145\/3419404","type":"journal-article","created":{"date-parts":[[2021,4,26]],"date-time":"2021-04-26T14:14:22Z","timestamp":1619446462000},"page":"86-95","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":23,"title":["Automata modulo theories"],"prefix":"10.1145","volume":"64","author":[{"given":"Loris","family":"D'Antoni","sequence":"first","affiliation":[{"name":"University of Wisconsin-Madison, WI"}]},{"given":"Margus","family":"Veanes","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, WA"}]}],"member":"320","published-online":{"date-parts":[[2021,4,26]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"DReX: A declarative language for efficiently evaluating regular string transformations. ACM SIGPLAN Notices -- POPL'15 50, 1","author":"Alur R","year":"2015","unstructured":"Alur , R , D'Antoni , L. , Raghothaman , M. DReX: A declarative language for efficiently evaluating regular string transformations. ACM SIGPLAN Notices -- POPL'15 50, 1 ( 2015 ), 125--137. Alur, R, D'Antoni, L., Raghothaman, M. DReX: A declarative language for efficiently evaluating regular string transformations. ACM SIGPLAN Notices -- POPL'15 50, 1 (2015), 125--137."},{"key":"e_1_2_1_2_1","first-page":"13","article-title":"Adding nesting structure to words. In Developments in Language Theory, O.H. Ibarra and Z. Dang, eds. Springer, Berlin","volume":"1","author":"Alur R.","year":"2006","unstructured":"Alur , R. , Madhusudan , P . Adding nesting structure to words. In Developments in Language Theory, O.H. Ibarra and Z. Dang, eds. Springer, Berlin , Heidelberg , 2006 , 1 -- 13 . Alur, R., Madhusudan, P. Adding nesting structure to words. In Developments in Language Theory, O.H. Ibarra and Z. Dang, eds. Springer, Berlin, Heidelberg, 2006, 1--13.","journal-title":"Heidelberg"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_23"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978383"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676986"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_14"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_1"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2018.03.017"},{"key":"e_1_2_1_9_1","volume-title":"Minimization of symbolic automata. ACM SIGPLAN Notices -- POPL'14 49, 1","author":"D'Antoni L.","year":"2014","unstructured":"D'Antoni , L. , Veanes , M. Minimization of symbolic automata. ACM SIGPLAN Notices -- POPL'14 49, 1 ( 2014 ), 541--553. D'Antoni, L., Veanes, M. Minimization of symbolic automata. ACM SIGPLAN Notices -- POPL'14 49, 1 (2014), 541--553."},{"key":"e_1_2_1_10_1","first-page":"1","article-title":"Extended symbolic finite automata and transducers","volume":"47","author":"D'Antoni L.","year":"2015","unstructured":"D'Antoni , L. , Veanes , M . Extended symbolic finite automata and transducers . Formal Methods Syst. Des. 47 , 1 ( Aug. 2015 ), 93--119. D'Antoni, L., Veanes, M. Extended symbolic finite automata and transducers. Formal Methods Syst. Des. 47, 1 (Aug. 2015), 93--119.","journal-title":"Formal Methods Syst. Des."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_30"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_3"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2791292"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1995376.1995394"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_10"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503291"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/321466.321473"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/2028067.2028068"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-12-417750-5.50022-1"},{"key":"e_1_2_1_22_1","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"Hopcroft J.E.","year":"1979","unstructured":"Hopcroft , J.E. , Ullman , J.D. Introduction to Automata Theory, Languages, and Computation . Addison Wesley, Reading , Mass , 1979 . Hopcroft, J.E., Ullman, J.D. Introduction to Automata Theory, Languages, and Computation. Addison Wesley, Reading, Mass, 1979."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062345"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90242-9"},{"key":"e_1_2_1_25_1","volume-title":"FSTTCS'14","author":"Keil M.","year":"2014","unstructured":"Keil , M. , Thiemann , P. Symbolic solving of extended regular expression inequalities . In FSTTCS'14 ( 2014 ), LIPIcs, Dagstuhl, Germany, 175--186. Keil, M., Thiemann, P. Symbolic solving of extended regular expression inequalities. In FSTTCS'14 (2014), LIPIcs, Dagstuhl, Germany, 175--186."},{"key":"e_1_2_1_26_1","first-page":"13","article-title":"A generic algorithm for learning symbolic automata from membership queries","volume":"11","author":"Maler O.","year":"2014","unstructured":"Maler , O. , Mens , I.-E . A generic algorithm for learning symbolic automata from membership queries . Logical Methods Comput. Sci. 11 , 3: 13 ( 2014 ), 2015. Maler, O., Mens, I.-E. A generic algorithm for learning symbolic automata from membership queries. Logical Methods Comput. Sci. 11, 3:13 (2014), 2015.","journal-title":"Logical Methods Comput. Sci."},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Maler O. Mens I.-E. Learning regular languages over large ordered alphabets. Log. Methods Comput. Sci. 11 3(2015)  Maler O. Mens I.-E. Learning regular languages over large ordered alphabets. Log. Methods Comput. Sci. 11 3(2015)","DOI":"10.2168\/LMCS-11(3:13)2015"},{"key":"e_1_2_1_28_1","first-page":"708","article-title":"Modular specification and efficient evaluation of quantitative queries over streaming data. ACM, New York","volume":"693","author":"Mamouras K.","year":"2017","unstructured":"Mamouras , K. , Raghotaman , M. , Alur , R. , Ives , Z.G. , Khanna , S. Stream QRE : Modular specification and efficient evaluation of quantitative queries over streaming data. ACM, New York , NY, USA , 2017 , 693 -- 708 . Mamouras, K., Raghotaman, M., Alur, R., Ives, Z.G., Khanna, S. StreamQRE: Modular specification and efficient evaluation of quantitative queries over streaming data. ACM, New York, NY, USA, 2017, 693--708.","journal-title":"NY, USA"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1515\/9781400882618-006"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1137\/0216062"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062362"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17462-0_24"},{"key":"e_1_2_1_34_1","first-page":"3","article-title":"On the equivalence and containment problems for unambiguous regular expressions, grammars, and automata","volume":"14","author":"Stearns R.E.","unstructured":"Stearns , R.E. , Hunt , H.B . On the equivalence and containment problems for unambiguous regular expressions, grammars, and automata . SIAM J. Comput. 14 , 3 , 598--611. Stearns, R.E., Hunt, H.B. On the equivalence and containment problems for unambiguous regular expressions, grammars, and automata. SIAM J. Comput. 14, 3, 598--611.","journal-title":"SIAM J. Comput."},{"key":"e_1_2_1_35_1","volume-title":"12th International Conference, CIAA 2007 (Prague, Czech Republic, July 16--18","author":"Vardi M.Y.","year":"2007","unstructured":"Vardi , M.Y. Linear-time model checking: Automata theory in practice. In Implementation and Application of Automata , 12th International Conference, CIAA 2007 (Prague, Czech Republic, July 16--18 , 2007 ), Revised Selected Papers, 5--10. Vardi, M.Y. Linear-time model checking: Automata theory in practice. In Implementation and Application of Automata, 12th International Conference, CIAA 2007 (Prague, Czech Republic, July 16--18, 2007), Revised Selected Papers, 5--10."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2010.15"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103674"},{"key":"e_1_2_1_38_1","volume-title":"Data-parallel string-manipulating programs. ACM SIGPLAN Notices -- POPL'15 50, 1","author":"Veanes M.","year":"2015","unstructured":"Veanes , M. , Mytkowicz , T. , Molnar , D. , Livshits , B. Data-parallel string-manipulating programs. ACM SIGPLAN Notices -- POPL'15 50, 1 ( 2015 ), 139--152. Veanes, M., Mytkowicz, T., Molnar, D., Livshits, B. Data-parallel string-manipulating programs. ACM SIGPLAN Notices -- POPL'15 50, 1 (2015), 139--152."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/319800.319808"},{"key":"e_1_2_1_40_1","volume-title":"Proceedings of the 35th International Conference on Machine Learning. J. Dy and A. Krause, eds.","volume":"80","author":"Weiss G.","year":"2018","unstructured":"Weiss , G. , Goldberg , Y. , Yahav , E. Extracting automata from recurrent neural networks using queries and counterexamples . In Proceedings of the 35th International Conference on Machine Learning. J. Dy and A. Krause, eds. Volume 80 , PMLR, Stockholmsmassan, Stockholm Sweden, 10- -15 Jul 2018 , 5247--5256 Weiss, G., Goldberg, Y., Yahav, E. Extracting automata from recurrent neural networks using queries and counterexamples. In Proceedings of the 35th International Conference on Machine Learning. J. Dy and A. Krause, eds. Volume 80, PMLR, Stockholmsmassan, Stockholm Sweden, 10--15 Jul 2018, 5247--5256"}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3419404","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3419404","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3419404","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:01:41Z","timestamp":1750197701000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3419404"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,4,26]]},"references-count":38,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2021,5]]}},"alternative-id":["10.1145\/3419404"],"URL":"https:\/\/doi.org\/10.1145\/3419404","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,4,26]]},"assertion":[{"value":"2021-04-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}