{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:29:46Z","timestamp":1784845786133,"version":"3.55.0"},"reference-count":178,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2021,11,23]],"date-time":"2021-11-23T00:00:00Z","timestamp":1637625600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Comput. Surv."],"published-print":{"date-parts":[[2023,1,31]]},"abstract":"<jats:p>String constraint solving refers to solving combinatorial problems involving constraints over string variables. String solving approaches have become popular over the past few years given the massive use of strings in different application domains like formal analysis, automated testing, database query processing, and cybersecurity.<\/jats:p><jats:p>This article reports a comprehensive survey on string constraint solving by exploring the large number of approaches that have been proposed over the past few decades to solve string constraints.<\/jats:p>","DOI":"10.1145\/3484198","type":"journal-article","created":{"date-parts":[[2021,11,23]],"date-time":"2021-11-23T17:36:59Z","timestamp":1637689019000},"page":"1-38","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":28,"title":["A Survey on String Constraint Solving"],"prefix":"10.1145","volume":"55","author":[{"given":"Roberto","family":"Amadini","sequence":"first","affiliation":[{"name":"University of Bologna, Bologna, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,11,23]]},"reference":[{"key":"e_1_3_2_2_2","unstructured":"[n.d.]. Chuffed a Lazy Clause Generation Solver. Retrieved from https:\/\/github.com\/chuffed\/chuffed."},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386034"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062384"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8602997"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_10"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_29"},{"key":"e_1_3_2_8_2","first-page":"1","volume-title":"Logic, Language, Information and Computation","author":"Alur Rajeev","year":"2011","unstructured":"Rajeev Alur. 2011. Streaming string transducers. In Logic, Language, Information and Computation, Lev D. Beklemishev and Ruy de Queiroz (Eds.). Springer, Berlin, 1\u20131."},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676981"},{"key":"e_1_3_2_10_2","unstructured":"Roberto Amadini. 2020. G-Strings: Gecode with (Dashed) String Variables. Retrieved from https:\/\/github.com\/ramadini\/gecode."},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-19212-9_1"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63139-4_4"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2018-1650"},{"key":"e_1_3_2_14_2","series-title":"Proceedings of the 24th European Conference on Artificial Intelligence (ECAI\/20), Including the 10th Conference on Prestigious Applications of Artificial Intelligence (PAIS\u201920)","first-page":"2875","volume":"325","author":"Amadini Roberto","year":"2020","unstructured":"Roberto Amadini, Graeme Gange, Peter Schachte, Harald S\u00f8ndergaard, and Peter J. Stuckey. 2020. String constraint solving: Past, present and future. In Proceedings of the 24th European Conference on Artificial Intelligence (ECAI\/20), Including the 10th Conference on Prestigious Applications of Artificial Intelligence (PAIS\u201920), Frontiers in Artificial Intelligence and Applications, Giuseppe De Giacomo, Alejandro Catal\u00e1, Bistra Dilkina, Michela Milano, Sen\u00e9n Barro, Alberto Bugar\u00edn, and J\u00e9r\u00f4me Lang (Eds.), Vol. 325. IOS Press, 2875\u20132876."},{"key":"e_1_3_2_15_2","unstructured":"Lecture Notes in Computer Science Proceedings of the 15th International Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming 10848 Roberto Amadini Graeme Gange Peter J. Stuckey W.-J. van Hoeve Propagating Lex Find and Replace with dashed strings 2018"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-98334-9_2"},{"key":"e_1_3_2_17_2","first-page":"6557","volume-title":"Proceedings of the 32nd AAAI Conference on Artificial Intelligence","author":"Amadini Roberto","year":"2018","unstructured":"Roberto Amadini, Graeme Gange, and Peter J. Stuckey. 2018. Sweep-based propagation for string constraint solving. In Proceedings of the 32nd AAAI Conference on Artificial Intelligence. AAAI Press, 6557\u20136564."},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-58475-7_1"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2020.103368"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66158-2_1"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_3"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_15"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236064"},{"key":"e_1_3_2_24_2","series-title":"NATO Science for Peace and Security Series, D: Information and Communication Security","first-page":"26","volume-title":"Dependable Software Systems Engineering","author":"Ball Thomas","year":"2015","unstructured":"Thomas Ball and Jakub Daniel. 2015. Deconstructing dynamic symbolic execution. In Dependable Software Systems Engineering, Maximilian Irlbeck, Doron A. Peled, and Alexander Pretschner (Eds.). NATO Science for Peace and Security Series, D: Information and Communication Security, Vol. 40. IOS Press, 26\u201341."},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2008.22"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950362"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-007-9036-6"},{"issue":"2","key":"e_1_3_2_28_2","first-page":"27","article-title":"Bringing CP, SAT and SMT together: Next challenges in constraint solving (dagstuhl seminar 19062)","volume":"9","author":"Bardin S\u00e9bastien","year":"2019","unstructured":"S\u00e9bastien Bardin, Nikolaj Bj\u00f8rner, and Cristian Cadar. 2019. Bringing CP, SAT and SMT together: Next challenges in constraint solving (dagstuhl seminar 19062). Dagstuhl Rep. 9, 2 (2019), 27\u201347. DOI:https:\/\/doi.org\/10.4230\/DagRep.9.2.27","journal-title":"Dagstuhl Rep."},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032319"},{"key":"e_1_3_2_30_2","unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2016. The Satisfiability Modulo Theories Library (SMT-LIB). Retrieved from https:\/\/www.SMT-LIB.org."},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ejc.2005.07.019"},{"key":"e_1_3_2_33_2","doi-asserted-by":"crossref","unstructured":"Murphy Berzish Joel D. Day Vijay Ganesh Mitja Kulczynski Florin Manea Federico Mora and Dirk Nowotka. 2021. String theories involving regular membership predicates: From practice to theory and back. Retrieved from https:\/\/arxiv.org\/abs\/2105.07220.","DOI":"10.1007\/978-3-030-85088-3_5"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102241"},{"key":"e_1_3_2_35_2","unstructured":"Murphy Berzish Mitja Kulczynski Federico Mora Florin Manea Joel D. Day Dirk Nowotka and Vijay Ganesh. 2020. A length-aware regular expression SMT solver. arxiv:2010.07253. Retrieved from https:\/\/arxiv.org\/abs\/2010.07253."},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046774"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_27"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_6"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14186-7_25"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106303"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68670-7"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-013-0332-x"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158091"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290362"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.5555\/267846.267852"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/11924661_23"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_1"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734089"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2018.00009"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1002\/spe.2218"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_53_2","unstructured":"Arlen Cox and Jason Leasure. 2017. Model checking regular language constraints. arxiv:1708.09073. Retrieved from http:\/\/arxiv.org\/abs\/1708.09073."},{"key":"e_1_3_2_54_2","first-page":"348","volume-title":"The Algebraic Theory of Automata","author":"Cin M. Dal","year":"1980","unstructured":"M. Dal Cin. 1980. The Algebraic Theory of Automata. Vieweg+Teubner Verlag, Wiesbaden, 348\u2013361."},{"key":"e_1_3_2_55_2","unstructured":"Loris D\u2019Antoni Anthony W. Lin and Philipp R\u00fcmmer. 2019. Meeting on String Constraints and Applications. Retrieved from https:\/\/mosca19.github.io\/."},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30806-3_8"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-00250-3_2"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/3372020.3391556"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02112533"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1145\/1273463.1273484"},{"key":"e_1_3_2_62_2","unstructured":"Julian Thom\u00e9 et al.[n.d.]. Joaco. Retrieved from https:\/\/sites.google.com\/site\/joacosite\/."},{"key":"e_1_3_2_63_2","unstructured":"Benjamin Fine Gerhard Rosenberger and Michael Stille. 2011. Nielsen transformations and applications: a survey. In Groups-Korea 94. De Gruyter 69\u2013106."},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.5555\/1506267"},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(98)10005-5"},{"key":"e_1_3_2_66_2","first-page":"535","volume-title":"Proceedings of the 22nd International Conference on Software Engineering & Knowledge Engineering (SEKE\u201910)","author":"Fu Xiang","year":"2010","unstructured":"Xiang Fu and Chung-Chih Li. 2010. A string constraint solver for detecting web application vulnerability. In Proceedings of the 22nd International Conference on Software Engineering & Knowledge Engineering (SEKE\u201910). Knowledge Systems Institute Graduate School, 535\u2013542."},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-011-0214-3"},{"key":"e_1_3_2_68_2","unstructured":"Vijay Ganesh and Murphy Berzish. 2016. Undecidability of a theory of strings linear arithmetic over length and string-number conversion. CoRR abs\/1605.09442 (2016). arXiv:1605.09442 http:\/\/arxiv.org\/abs\/1605.09442."},{"key":"e_1_3_2_69_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_52"},{"key":"e_1_3_2_70_2","series-title":"Proceedings of the 8th International Haifa Verification Conference on Hardware and Software: Verification and Testing (HVC\u201912). Revised Selected Papers.","first-page":"209","volume":"7857","author":"Ganesh Vijay","year":"2012","unstructured":"Vijay Ganesh, Mia Minnes, Armando Solar-Lezama, and Martin C. Rinard. 2012. Word equations with length constraints: What\u2019s decidable? In Proceedings of the 8th International Haifa Verification Conference on Hardware and Software: Verification and Testing (HVC\u201912). Revised Selected Papers.Lecture Notes in Computer Science, Armin Biere, Amir Nahir, and Tanja E. J. Vos (Eds.), Vol. 7857. Springer, 209\u2013226."},{"key":"e_1_3_2_71_2","unstructured":"Graeme Gange. [n.d.]. smt2mzn-str. Available at https:\/\/bitbucket.org\/gkgange\/smt2mzn-str."},{"key":"e_1_3_2_72_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_20"},{"key":"e_1_3_2_73_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_14"},{"key":"e_1_3_2_74_2","unstructured":"Gecode Team. 2016. Gecode: Generic Constraint Development Environment. Retrieved from http:\/\/www.gecode.org."},{"key":"e_1_3_2_75_2","doi-asserted-by":"publisher","DOI":"10.1070\/RM1961v016n05ABEH004112"},{"key":"e_1_3_2_76_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45193-8_26"},{"key":"e_1_3_2_77_2","unstructured":"Google. [n.d.]. OR-Tools. Retrieved from https:\/\/developers.google.com\/optimization."},{"key":"e_1_3_2_78_2","doi-asserted-by":"publisher","DOI":"10.1145\/3242953.3242964"},{"key":"e_1_3_2_79_2","first-page":"217","volume-title":"Proceedings of the 22nd AAAI Conference on Artificial Intelligence","author":"Hansen Esben Rune","year":"2007","unstructured":"Esben Rune Hansen and Henrik Reif Andersen. 2007. Interactive configuration with regular string constraints. In Proceedings of the 22nd AAAI Conference on Artificial Intelligence. AAAI Press, 217\u2013223."},{"key":"e_1_3_2_80_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40627-0_31"},{"key":"e_1_3_2_81_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-34175-6_2"},{"key":"e_1_3_2_82_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158092"},{"key":"e_1_3_2_83_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_18"},{"key":"e_1_3_2_84_2","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542498"},{"key":"e_1_3_2_85_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-012-0111-x"},{"key":"e_1_3_2_86_2","doi-asserted-by":"publisher","DOI":"10.5555\/1454320"},{"key":"e_1_3_2_87_2","unstructured":"IBM. 2018. Security AppScan. Retrieved from https:\/\/www.ibm.com\/security\/application-security\/appscan."},{"key":"e_1_3_2_88_2","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)90033-7"},{"key":"e_1_3_2_89_2","doi-asserted-by":"publisher","DOI":"10.1145\/2743014"},{"issue":"6","key":"e_1_3_2_90_2","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1109\/TC.1978.1675141","article-title":"Binary decision diagrams","volume":"27","author":"Jr. Sheldon B. Akers,","year":"1978","unstructured":"Sheldon B. Akers, Jr.1978. Binary decision diagrams. IEEE Trans. Comput. 27, 6 (1978), 509\u2013516. DOI:https:\/\/doi.org\/10.1109\/TC.1978.1675141","journal-title":"IEEE Trans. Comput."},{"key":"e_1_3_2_91_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-009-9073-4"},{"key":"e_1_3_2_92_2","doi-asserted-by":"publisher","DOI":"10.1145\/2642937.2643003"},{"key":"e_1_3_2_93_2","doi-asserted-by":"publisher","DOI":"10.1145\/2377656.2377662"},{"key":"e_1_3_2_94_2","doi-asserted-by":"publisher","DOI":"10.1145\/1572272.1572286"},{"key":"e_1_3_2_95_2","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_96_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028022"},{"key":"e_1_3_2_97_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.798326"},{"key":"e_1_3_2_98_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-50137-6_7"},{"key":"e_1_3_2_99_2","series-title":"Proceedings of the Conference on Declarative Programming on Declarative Programming and Knowledge Management, (DECLARE\u201919), Revised Selected Papers","first-page":"139","volume":"12057","author":"Krings Sebastian","year":"2019","unstructured":"Sebastian Krings, Joshua Schmidt, Patrick Skowronek, Jannik Dunkelau, and Dierk Ehmke. 2019. Towards constraint logic programming over strings for test data generation. In Proceedings of the Conference on Declarative Programming on Declarative Programming and Knowledge Management, (DECLARE\u201919), Revised Selected Papers, Lecture Notes in Computer Science, Petra Hofstedt, Salvador Abreu, Ulrich John, Herbert Kuchen, and Dietmar Seipel (Eds.), Vol. 12057. Springer, 139\u2013159."},{"key":"e_1_3_2_100_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-44953-1_45"},{"key":"e_1_3_2_101_2","series-title":"Proceedings of the 14th Conference on Artificial Intelligence in Medicine on Artificial Intelligence in Medicine (AIME\u201913),","first-page":"110","volume":"7885","author":"Krippahl Ludwig","unstructured":"Ludwig Krippahl, F\u00e1bio Madeira, and Pedro Barahona. [n.d.]. Constraining protein docking with coevolution data for medical research. In Proceedings of the 14th Conference on Artificial Intelligence in Medicine on Artificial Intelligence in Medicine (AIME\u201913),Lecture Notes in Computer Science, Niels Peek, Roque Mar\u00edn Morales, and Mor Peleg (Eds.), Vol. 7885. Springer, 110\u2013114."},{"key":"e_1_3_2_102_2","doi-asserted-by":"publisher","DOI":"10.1145\/3387903.3389317"},{"issue":"141","key":"e_1_3_2_103_2","first-page":"82","article-title":"On semigroups","volume":"36","author":"Levi Frank W.","year":"1944","unstructured":"Frank W. Levi. 1944. On semigroups. Bull. Calcutta Math. Soc 36, 141\u2013146 (1944), 82.","journal-title":"Bull. Calcutta Math. Soc"},{"key":"e_1_3_2_104_2","first-page":"15","volume-title":"Proc. 9th Int. Haifa Verification Conf.","author":"Li Guodong","year":"2013","unstructured":"Guodong Li and Indradeep Ghosh. 2013. PASS: String solving with parameterized array and interval automaton. In Proc. 9th Int. Haifa Verification Conf. Lecture Notes in Computer Science, V. Bertacco and A. Legay (Eds.), Vol. 8244. Springer, 15\u201331."},{"key":"e_1_3_2_105_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_43"},{"key":"e_1_3_2_106_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24246-0_9"},{"key":"e_1_3_2_107_2","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837641"},{"key":"e_1_3_2_108_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_21"},{"key":"e_1_3_2_109_2","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314645"},{"key":"e_1_3_2_110_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511566097"},{"key":"e_1_3_2_111_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107341005"},{"key":"e_1_3_2_112_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107326019"},{"key":"e_1_3_2_113_2","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594331"},{"key":"e_1_3_2_114_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54807-9_12"},{"key":"e_1_3_2_115_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-01929-6_13"},{"issue":"2","key":"e_1_3_2_116_2","first-page":"147","article-title":"The problem of solvability of equations in a free semigroup","volume":"145","author":"Makanin Gennadiy Semenovich","year":"1977","unstructured":"Gennadiy Semenovich Makanin. 1977. The problem of solvability of equations in a free semigroup. Mat. Sbornik 145, 2 (1977), 147\u2013236.","journal-title":"Mat. Sbornik"},{"key":"e_1_3_2_117_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33558-7_39"},{"key":"e_1_3_2_118_2","doi-asserted-by":"publisher","DOI":"10.1145\/1060745.1060809"},{"key":"e_1_3_2_119_2","unstructured":"Yasuhiko Minamide and Nobuo Otoi. [n.d.]. PHP String Analyzer. Retrieved from https:\/\/sv.c.titech.ac.jp\/minamide\/phpsa\/."},{"key":"e_1_3_2_120_2","first-page":"153","volume-title":"Regular Approximation of Context-Free Grammars through Transformation","author":"Mohri Mehryar","year":"2001","unstructured":"Mehryar Mohri and Mark-Jan Nederhof. 2001. Regular Approximation of Context-Free Grammars through Transformation. Springer Netherlands, Dordrecht, 153\u2013163."},{"key":"e_1_3_2_121_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74970-7_38"},{"key":"e_1_3_2_122_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-008-9064-x"},{"key":"e_1_3_2_123_2","doi-asserted-by":"publisher","DOI":"10.1145\/2989225.2989228"},{"key":"e_1_3_2_124_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30201-8_36"},{"key":"e_1_3_2_125_2","doi-asserted-by":"publisher","DOI":"10.1145\/990308.990312"},{"key":"e_1_3_2_126_2","doi-asserted-by":"publisher","DOI":"10.1145\/1132516.1132584"},{"key":"e_1_3_2_127_2","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9904-1946-08555-9"},{"key":"e_1_3_2_128_2","unstructured":"Py-Conbyte Team. 2021. Py-Conbyte: A Python Concolic Testing Tool Running on Bytecode Level. Retrieved from https:\/\/github.com\/spencerwuwu\/py-conbyte."},{"key":"e_1_3_2_129_2","doi-asserted-by":"publisher","DOI":"10.1007\/11889205_64"},{"key":"e_1_3_2_130_2","doi-asserted-by":"publisher","DOI":"10.2307\/2268308"},{"key":"e_1_3_2_131_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58601-6_94"},{"key":"e_1_3_2_132_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_2"},{"key":"e_1_3_2_133_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51074-9_13"},{"key":"e_1_3_2_134_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_24"},{"key":"e_1_3_2_135_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49116-3_20"},{"key":"e_1_3_2_136_2","doi-asserted-by":"publisher","DOI":"10.5555\/2843512"},{"key":"e_1_3_2_137_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89439-1_20"},{"key":"e_1_3_2_138_2","doi-asserted-by":"publisher","DOI":"10.5555\/578864"},{"key":"e_1_3_2_139_2","doi-asserted-by":"publisher","DOI":"10.5555\/2337223.2337257"},{"key":"e_1_3_2_140_2","unstructured":"Prateek Saxena and Devdatta Akhawe. [n.d.]. Kaluza String Solver. Retrieved from http:\/\/webblaze.cs.berkeley.edu\/2010\/kaluza\/."},{"key":"e_1_3_2_141_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.38"},{"key":"e_1_3_2_142_2","unstructured":"Joseph Scott. [n.d.]. Prototype Implementation of a Bounded String Module for the Gecode CP Library. Retrieved from https:\/\/github.com\/jossco\/gecode-string."},{"key":"e_1_3_2_143_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-63618-0_5"},{"key":"e_1_3_2_144_2","volume-title":"Other Things Besides Number: Abstraction, Constraint Propagation, and String Variable Types","author":"Scott Joseph D.","year":"2016","unstructured":"Joseph D. Scott. 2016. Other Things Besides Number: Abstraction, Constraint Propagation, and String Variable Types. Ph.D. Dissertation. Department of Information Technology, Uppsala University, Sweden."},{"key":"e_1_3_2_145_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICTAI.2013.155"},{"key":"e_1_3_2_146_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-18008-3_26"},{"key":"e_1_3_2_147_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-59776-8_5"},{"key":"e_1_3_2_148_2","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(95)00034-H"},{"key":"e_1_3_2_149_2","volume-title":"Symbolic Boolean Derivatives for Efficiently Solving Extended Regular Expression Constraints","author":"Stanford Caleb","year":"2020","unstructured":"Caleb Stanford, Margus Veanes, and Nikolaj Bjorner. 2020. Symbolic Boolean Derivatives for Efficiently Solving Extended Regular Expression Constraints. Technical Report MSR-TR-2020-25. Microsoft."},{"key":"e_1_3_2_150_2","unstructured":"Jari Stenman. [n.d.]. Norn a Solver for String Constraints. Retrieved from http:\/\/user.it.uu.se\/ jarst116\/norn\/."},{"issue":"2","key":"e_1_3_2_151_2","first-page":"55","article-title":"The minizinc challenge 2008-2013","author":"Stuckey Peter J.","year":"2014","unstructured":"Peter J. Stuckey, Thibaut Feydy, Andreas Schutt, Guido Tack, and Julien Fischer. 2014. The minizinc challenge 2008-2013. AI Mag.2 (2014), 55\u201360.","journal-title":"AI Mag."},{"key":"e_1_3_2_152_2","article-title":"A solver for a theory of strings and bit-vectors","volume":"1605","author":"Subramanian Sanu","year":"2016","unstructured":"Sanu Subramanian, Murphy Berzish, Yunhui Zheng, Omer Tripp, and Vijay Ganesh. 2016. A solver for a theory of strings and bit-vectors. CoRR abs\/1605.09446. Retrieved from http:\/\/arxiv.org\/abs\/1605.09446.","journal-title":"CoRR"},{"key":"e_1_3_2_153_2","doi-asserted-by":"publisher","DOI":"10.5555\/1855083"},{"key":"e_1_3_2_154_2","doi-asserted-by":"publisher","DOI":"10.1145\/2522920.2522926"},{"key":"e_1_3_2_155_2","unstructured":"BRICS team. [n.d.]. Java String Analyzer. Retrieved from https:\/\/www.brics.dk\/JSA."},{"key":"e_1_3_2_156_2","unstructured":"BRICS team. [n.d.]. The MONA Project. Retrieved from https:\/\/www.brics.dk\/mona."},{"key":"e_1_3_2_157_2","unstructured":"Z3 team. [n.d.]. Z3 Solver. Retrieved from https:\/\/github.com\/Z3Prover\/Z3."},{"key":"e_1_3_2_158_2","unstructured":"Z3 team. [n.d.]. Z3str4 Description. Retrieved from https:\/\/z3str4.github.io\/smtcomp.pdf."},{"key":"e_1_3_2_159_2","unstructured":"Z3 team. [n.d.]. Z3str4 String Solver. Retrieved from https:\/\/z3str4.github.io\/."},{"key":"e_1_3_2_160_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2017.26"},{"key":"e_1_3_2_161_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_49"},{"key":"e_1_3_2_162_2","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660372"},{"key":"e_1_3_2_163_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_12"},{"key":"e_1_3_2_164_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_21"},{"key":"e_1_3_2_165_2","unstructured":"Min-Thai Trinh. [n.d.]. S3: An Efficient String Solver and Model Counter. Retrieved from https:\/\/trinhmt.github.io\/home\/S3\/."},{"key":"e_1_3_2_166_2","doi-asserted-by":"publisher","DOI":"10.1070\/SM1983v044n01ABEH000954"},{"key":"e_1_3_2_167_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39274-0_3"},{"key":"e_1_3_2_168_2","doi-asserted-by":"crossref","unstructured":"Margus Veanes and Peli de Halleux. [n.d.]. Rex\u2014Regular Expression Exploration. Retrieved from https:\/\/rise4fun.com\/rex.","DOI":"10.1109\/ICST.2010.15"},{"key":"e_1_3_2_169_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2010.15"},{"key":"e_1_3_2_170_2","unstructured":"Pavol Voda. 1988. The Constraint Language Trilogy: Semantics and Computations . Technical Report. Complete Logic Systems North Vancouver BC Canada."},{"key":"e_1_3_2_171_2","volume-title":"Cerebral Mechanisms in Behaviour","author":"Neumann J. von","year":"1951","unstructured":"J. von Neumann. 1951. The general and logical theory of automata. In Cerebral Mechanisms in Behaviour, L. A. Jeffress (Ed.). Wiley."},{"key":"e_1_3_2_172_2","first-page":"181","volume-title":"Proceedings of the 6th International Conference on Logic Programming","author":"Walinsky Clifford","year":"1989","unstructured":"Clifford Walinsky. 1989. CLP(Sigma*): Constraint logic programming with regular sets. In Proceedings of the 6th International Conference on Logic Programming, Giorgio Levi and Maurizio Martelli (Eds.). MIT Press, 181\u2013196."},{"key":"e_1_3_2_173_2","series-title":"Proceedings of the 28th International Conference on Computer Aided Verification(CAV\u201916) Part I,","first-page":"241","volume":"9779","author":"Wang Hung-En","year":"2016","unstructured":"Hung-En Wang, Tzung-Lin Tsai, Chun-Han Lin, Fang Yu, and Jie-Hong R. Jiang. 2016. String analysis via automata manipulation with logic circuit representation. In Proceedings of the 28th International Conference on Computer Aided Verification(CAV\u201916) Part I,Lecture Notes in Computer Science, Swarat Chaudhuri and Azadeh Farzan (Eds.), Vol. 9779. Springer, 241\u2013260."},{"issue":"1","key":"e_1_3_2_174_2","first-page":"221","article-title":"The SMT competition 2015-2018","volume":"11","author":"Weber Tjark","year":"2019","unstructured":"Tjark Weber, Sylvain Conchon, David D\u00e9harbe, Matthias Heizmann, Aina Niemetz, and Giles Reger. 2019. The SMT competition 2015-2018. J. Satisf. Bool. Model. Comput. 11, 1 (2019), 221\u2013259. https:\/\/doi.org\/10.3233\/SAT190123","journal-title":"J. Satisf. Bool. Model. Comput."},{"key":"e_1_3_2_175_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_13"},{"key":"e_1_3_2_176_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0263-6"},{"key":"e_1_3_2_177_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_14"},{"key":"e_1_3_2_178_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491456"},{"key":"e_1_3_2_179_2","first-page":"810","article-title":"Solving string constraints with streaming string transducers","volume":"27","author":"Zhu Qizhen","year":"2019","unstructured":"Qizhen Zhu, Hitoshi Akama, and Yasuhiko Minamide. 2019. Solving string constraints with streaming string transducers. J. Inf. Process. 27 (2019), 810\u2013821.","journal-title":"J. Inf. Process."}],"container-title":["ACM Computing Surveys"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3484198","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3484198","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:17:13Z","timestamp":1750191433000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3484198"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,23]]},"references-count":178,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,1,31]]}},"alternative-id":["10.1145\/3484198"],"URL":"https:\/\/doi.org\/10.1145\/3484198","relation":{},"ISSN":["0360-0300","1557-7341"],"issn-type":[{"value":"0360-0300","type":"print"},{"value":"1557-7341","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,11,23]]},"assertion":[{"value":"2020-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-11-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}