{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T22:30:16Z","timestamp":1783549816023,"version":"3.55.0"},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101089343"],"award-info":[{"award-number":["101089343"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004281","name":"Narodowe Centrum Nauki","doi-asserted-by":"publisher","award":["2017\/26\/E\/ST6\/00191"],"award-info":[{"award-number":["2017\/26\/E\/ST6\/00191"]}],"id":[{"id":"10.13039\/501100004281","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>Parikh\u2019s Theorem is a fundamental result in automata theory with numerous applications in computer science. These include software verification (e.g. infinite-state verification, string constraints, and theory of arrays), verification of cryptographic protocols (e.g. using Horn clauses modulo equational theories) and database querying (e.g. evaluating path-queries in graph databases), among others. Parikh\u2019s Theorem states that the letter-counting abstraction of a language recognized by finite automata or context-free grammars is definable in Linear Integer Arithmetic (a.k.a. Presburger Arithmetic). In fact, there is a linear-time algorithm computing existential Presburger formulas capturing such abstractions, which enables an efficient analysis via SMT-solvers. Unfortunately, real-world applications typically require large alphabets (e.g. Unicode, containing a million of characters) \u2014 which are well-known to be not amenable to explicit treatment of the alphabets \u2014 or even worse infinite alphabets.<\/jats:p>\n          <jats:p>Symbolic automata have proven in the last decade to be an effective algorithmic framework for handling large finite or even infinite alphabets. A symbolic automaton employs an effective boolean algebra, which offers a symbolic representation of character sets (i.e. in terms of predicates) and often lends itself to an exponentially more succinct representation of a language. Instead of letter-counting, Parikh\u2019s Theorem for symbolic automata amounts to counting the number of times different predicates are satisfied by an input sequence. Unfortunately, naively applying Parikh\u2019s Theorem from classical automata theory to symbolic automata yields existential Presburger formulas of exponential size. In this paper, we provide a new construction for Parikh\u2019s Theorem for symbolic automata and grammars, which avoids this exponential blowup: our algorithm computes an existential formula in polynomial-time over (quantifier-free) Presburger and the base theory. In fact, our algorithm extends to the model of parametric symbolic grammars, which are one of the most expressive models of languages over infinite alphabets. We have implemented our algorithm and show it can be used to solve string constraints that are difficult to solve by existing solvers.<\/jats:p>","DOI":"10.1145\/3632907","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"1945-1977","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Parikh\u2019s Theorem Made Symbolic"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4913-3800","authenticated-orcid":false,"given":"Matthew","family":"Hague","sequence":"first","affiliation":[{"name":"Royal Holloway, University of London, Egham, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4321-3105","authenticated-orcid":false,"given":"Artur","family":"Je\u017c","sequence":"additional","affiliation":[{"name":"University of Wroclaw, Wroclaw, Poland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4715-5096","authenticated-orcid":false,"given":"Anthony W.","family":"Lin","sequence":"additional","affiliation":[{"name":"University of Kaiserslautern-Landau, Kaiserslautern, Germany"},{"name":"Max-Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062384"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8602997"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_10"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31784-3_16"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-19212-9_1"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2389241.2389250"},{"key":"e_1_3_1_9_1","volume-title":"H3 mit Gleichheitstheorien","author":"Barner S.","year":"2006","unstructured":"S. Barner. 2006. H3 mit Gleichheitstheorien. Diploma Thesis. Technische Universitaet Muenchen."},{"key":"e_1_3_1_10_1","volume-title":"The SMT-LIB Standard: Version 2.6","author":"Barrett Clark","year":"2017","unstructured":"Clark Barrett, Pascal Fontaine, and Cesare Tinelli. 2017. The SMT-LIB Standard: Version 2.6. Technical Report. Department of Computer Science, The University of Iowa. Available at www.SMT-LIB.org."},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_3"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_23"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604137"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2019.107"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498707"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59152-6_18"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290362"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_1"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_13"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_14"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_1"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_3"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3419404"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2338626.2338632"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.orl.2005.09.008"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.3233\/FI-1997-3112"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926443"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-38919-2_14"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3517804.3524159"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533354"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-17524-9_31"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.01.026"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13089-2_47"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_60"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_22"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470626"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45093-9_59"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37703-7_2"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.21"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1844-9"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74105-3"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2010.20"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(1:3)2013"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837641"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28872-2_25"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314645"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1060745.1060809"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009879"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591262"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/321356.321364"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183440.3194964"},{"key":"e_1_3_1_54_1","unstructured":"Rodrigo Raya. 2023. The Complexity of Checking Non-Emptiness in Symbolic Tree Automata. Retrieved October 25 2023 from https:\/\/infoscience.epfl.ch\/record\/304426"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.38"},{"key":"e_1_3_1_56_1","volume-title":"Introduction to the Theory of Computation","author":"Sipser Michael","year":"2013","unstructured":"Michael Sipser. 2013. Introduction to the Theory of Computation (third ed.). Course Technology, Boston, MA."},{"key":"e_1_3_1_57_1","unstructured":"SMTCOMP2022 2022. The International Satisfiability Modulo Theories (SMT) Competition 2022. https:\/\/smt-comp.github.io\/2022\/ Accessed: 7 July 2023."},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454066"},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","unstructured":"SymParikh Artifact 2023. Parikh\u2019s Theorem Made Symbolic: Artifact. https:\/\/doi.org\/10.5281\/zenodo.10125861 10.5281\/zenodo.10125861 Accessed: 23 October 2023.","DOI":"10.5281\/zenodo.10125861"},{"key":"e_1_3_1_60_1","unstructured":"SymParikh Repository 2023. Parikh\u2019s Theorem Made Symbolic. https:\/\/gitlab.cim.rhul.ac.uk\/uxac009\/symparikh Accessed: 23 October 2023."},{"key":"e_1_3_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04027-6_35"},{"key":"e_1_3_1_62_1","unstructured":"UUVerifiers 2023. OSTRICH. https:\/\/github.com\/uuverifiers\/ostrich Accessed: 12 June 2023."},{"key":"e_1_3_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103621.2103674"},{"key":"e_1_3_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_25"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632907","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632907","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:01:56Z","timestamp":1751659316000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632907"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":63,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632907"],"URL":"https:\/\/doi.org\/10.1145\/3632907","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}