{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T09:31:40Z","timestamp":1770975100811,"version":"3.50.1"},"reference-count":73,"publisher":"Springer Science and Business Media LLC","issue":"1-4","license":[{"start":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T00:00:00Z","timestamp":1747785600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T00:00:00Z","timestamp":1747785600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001823","name":"Ministerstvo \u0160kolstv\u00ed, Ml\u00e1de\u017ee a T\u011blov\u00fdchovy","doi-asserted-by":"publisher","award":["LL1908"],"award-info":[{"award-number":["LL1908"]}],"id":[{"id":"10.13039\/501100001823","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001824","name":"Grantov\u00e1 Agentura \u010cesk\u00e9 Republiky","doi-asserted-by":"publisher","award":["GA23-07565S"],"award-info":[{"award-number":["GA23-07565S"]}],"id":[{"id":"10.13039\/501100001824","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004663","name":"Ministry of Science and Technology, Taiwan","doi-asserted-by":"publisher","award":["109-2628-E-001-001-MY3"],"award-info":[{"award-number":["109-2628-E-001-001-MY3"]}],"id":[{"id":"10.13039\/501100004663","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Brno University of Technology"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Constraints"],"published-print":{"date-parts":[[2025,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We propose a new automata-based algorithm for solving string constraints that tightly integrates reasoning about equations and regular constraints. Exchanging information between the two allows an efficient pruning of generated combinatorial cases. The algorithm is based on a novel language-based characterization of satisfiability of word equations with regular constraints. Namely, satisfiability of an equation is implied by its\n                    <jats:italic>stability<\/jats:italic>\n                    : the concatenation of the regular languages constraining variables on the left-hand side equals the concatenation of the languages on the right-hand side. It is complete for the chain-free string constraints. We experimentally show that our prototype implementation is competitive with the best string solvers and even superior on difficult examples.\n                  <\/jats:p>","DOI":"10.1007\/s10601-025-09379-w","type":"journal-article","created":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T08:00:01Z","timestamp":1747814401000},"page":"1-34","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Word equations in synergy with regular constraints (extended version)"],"prefix":"10.1007","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1880-5379","authenticated-orcid":false,"given":"Franti\u0161ek","family":"Blahoudek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2872-0336","authenticated-orcid":false,"given":"Yu-Fang","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-5614-1592","authenticated-orcid":false,"given":"David","family":"Chocholat\u00fd","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4375-7954","authenticated-orcid":false,"given":"Vojt\u011bch","family":"Havlena","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6957-1651","authenticated-orcid":false,"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3038-5875","authenticated-orcid":false,"given":"Ond\u0159ej","family":"Leng\u00e1l","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7454-3751","authenticated-orcid":false,"given":"Juraj","family":"S\u00ed\u010d","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,21]]},"reference":[{"key":"9379_CR1","unstructured":"OWASP, Top 10. https:\/\/www.owasp.org\/images\/f\/f8\/OWASP_Top_10_-_2013.pdf (2013)."},{"key":"9379_CR2","unstructured":"OWASP, Top 10. https:\/\/owasp.org\/www-project-top-ten\/2017\/ (2017)."},{"key":"9379_CR3","unstructured":"OWASP, Top 10. https:\/\/owasp.org\/Top10\/ (2021)."},{"key":"9379_CR4","unstructured":"Hadarean, L. (2019). String solving at Amazon. https:\/\/mosca19.github.io\/program\/index.html. Presented at MOSCA\u201919."},{"key":"9379_CR5","doi-asserted-by":"publisher","unstructured":"Alt, L., Blicha, M., Hyv\u00e4rinen, A.\u00a0E.\u00a0J., & Sharygina, N. (2022). SolCMC: Solidity compiler\u2019s model checker. In S.\u00a0Shoham, & Y.\u00a0Vizel (Eds.), Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I, Vol. 13371 of Lecture Notes in Computer Science (pp. 325\u2013338). Springer. https:\/\/doi.org\/10.1007\/978-3-031-13185-1_16","DOI":"10.1007\/978-3-031-13185-1_16"},{"key":"9379_CR6","doi-asserted-by":"publisher","first-page":"646","DOI":"10.1007\/978-3-319-08867-9_43","volume-title":"Computer Aided Verification","author":"T Liang","year":"2014","unstructured":"Liang, T., Reynolds, A., Tinelli, C., Barrett, C., & Deters, M. (2014). A DPLL(T) theory solver for a theory of strings and regular expressions. In A. Biere & R. Bloem (Eds.), Computer Aided Verification (pp. 646\u2013662). Cham: Springer International Publishing."},{"issue":"3","key":"9379_CR7","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/s10703-016-0247-6","volume":"48","author":"T Liang","year":"2016","unstructured":"Liang, T., Reynolds, A., Tsiskaridze, N., Tinelli, C., Barrett, C., & Deters, M. (2016). An efficient SMT solver for string constraints. Formal Methods in System Design, 48(3), 206\u2013234.","journal-title":"Formal Methods in System Design"},{"key":"9379_CR8","doi-asserted-by":"crossref","unstructured":"Barrett, C.\u00a0W., Tinelli, C., Deters, M., Liang, T., Reynolds, A., & Tsiskaridze, N. (2016). Efficient solving of string constraints for security analysis. In HotSoS\u201916, ACM Transactions on Computational Logic (pp. 4\u20136).","DOI":"10.1145\/2898375.2898393"},{"key":"9379_CR9","doi-asserted-by":"crossref","unstructured":"Liang, T., Tsiskaridze, N., Reynolds, A., Tinelli, C., & Barrett, C. (2015). A decision procedure for regular membership and length constraints over unbounded strings. In FroCoS\u201915, Vol. 9322 of LNCS (pp. 135\u2013150). Springer.","DOI":"10.1007\/978-3-319-24246-0_9"},{"key":"9379_CR10","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-319-63390-9_24","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2017","unstructured":"Reynolds, A., Woo, M., Barrett, C., Brumley, D., Liang, T., & Tinelli, C. (2017). Scaling up DPLL(T) string solvers using context-dependent simplification. In R. Majumdar & V. Kun\u010dak (Eds.), Computer Aided Verification (pp. 453\u2013474). Cham: Springer International Publishing."},{"key":"9379_CR11","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/978-3-031-13188-2_11","volume-title":"Computer Aided Verification","author":"A N\u00f6tzli","year":"2022","unstructured":"N\u00f6tzli, A., Reynolds, A., Barbosa, H., Barrett, C., & Tinelli, C. (2022). Even faster conflicts and lazier reductions for string solvers. In S. Shoham & Y. Vizel (Eds.), Computer Aided Verification (pp. 205\u2013226). Cham: Springer International Publishing."},{"key":"9379_CR12","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Notzlit, A., Barrett, C., & Tinelli, C. (2020). Reductions for strings and regular expressions revisited. In 2020 Formal Methods in Computer Aided Design (FMCAD) (pp. 225\u2013235). https:\/\/doi.org\/10.34727\/2020\/isbn.978-3-85448-042-6_30","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_30"},{"key":"9379_CR13","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., N\u00f6tzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., & Zohar, Y. (2022). cvc5: A versatile and industrial-strength smt solver. In D. Fisman & G. Rosu (Eds.), Tools and Algorithms for the Construction and Analysis of Systems (pp. 415\u2013442). Cham: Springer International Publishing."},{"key":"9379_CR14","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., Tillmann, N., & Voronkov, A. (2009). Path feasibility analysis for string-manipulating programs. In TACAS\u201909, Vol. 5505 of LNCS (pp. 307\u2013321). Springer.","DOI":"10.1007\/978-3-642-00768-2_27"},{"key":"9379_CR15","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., & Bj\u00f8rner, N. (2008). Z3: An efficient smt solver. In C. R. Ramakrishnan & J. Rehof (Eds.), Tools and Algorithms for the Construction and Analysis of Systems (pp. 337\u2013340). Berlin Heidelberg, Berlin, Heidelberg: Springer."},{"key":"9379_CR16","doi-asserted-by":"crossref","unstructured":"Zheng, Y., Zhang, X., & Ganesh, V. (2013). Z3-str: A Z3-based string solver for web application analysis. In ESEC\/FSE\u201913, ACM Transactions on Computational Logic (pp. 114\u2013124).","DOI":"10.1145\/2491411.2491456"},{"key":"9379_CR17","doi-asserted-by":"publisher","unstructured":"Berzish, M., Ganesh, V., & Zheng, Y. (2017). Z3str3: A string solver with theory-aware heuristics. In Formal Methods in Computer Aided Design (FMCAD) (pp. 55\u201359). https:\/\/doi.org\/10.23919\/FMCAD.2017.8102241","DOI":"10.23919\/FMCAD.2017.8102241"},{"key":"9379_CR18","unstructured":"Berzish, M. (2021). Z3str4: A solver for theories over strings, Ph.D. thesis. http:\/\/hdl.handle.net\/10012\/17102"},{"key":"9379_CR19","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-319-21690-4_14","volume-title":"Computer Aided Verification","author":"Y Zheng","year":"2015","unstructured":"Zheng, Y., Ganesh, V., Subramanian, S., Tripp, O., Dolby, J., & Zhang, X. (2015). Effective search-space pruning for solvers of string equations, regular expressions and length constraints. In D. Kroening & C. S. P\u0103s\u0103reanu (Eds.), Computer Aided Verification (pp. 235\u2013254). Cham: Springer International Publishing."},{"key":"9379_CR20","doi-asserted-by":"publisher","unstructured":"Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J.\u00a0D., Nowotka, D., & Ganesh, V. (2021). An SMT solver for regular expressions and linear arithmetic over string length. In A.\u00a0Silva, & K.\u00a0R.\u00a0M. Leino (Eds.), Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II, Vol. 12760 of Lecture Notes in Computer Science (pp. 289\u2013312). Springer. https:\/\/doi.org\/10.1007\/978-3-030-81688-9_14","DOI":"10.1007\/978-3-030-81688-9_14"},{"key":"9379_CR21","doi-asserted-by":"crossref","unstructured":"Lin, A.\u00a0W., & Barcel\u00f3, P. (2016). String solving with word equations and transducers: Towards a logic for analysing mutation XSS. In POPL\u201916, ACM Transactions on Computational Logic. (pp. 123\u2013136).","DOI":"10.1145\/2837614.2837641"},{"issue":"POPL","key":"9379_CR22","doi-asserted-by":"publisher","first-page":"3:1","DOI":"10.1145\/3158091","volume":"2","author":"T Chen","year":"2018","unstructured":"Chen, T., Chen, Y., Hague, M., Lin, A. W., & Wu, Z. (2018). What is decidable about string constraints with the replaceall function. Proceedings of ACM Programming Languages, 2(POPL), 3:1-3:29. https:\/\/doi.org\/10.1145\/3158091","journal-title":"Proceedings of ACM Programming Languages"},{"key":"9379_CR23","doi-asserted-by":"publisher","unstructured":"Chen, T., Hague, M., Lin, A. W., R\u00fcmmer, P., & Wu, Z. (2019). Decision procedures for path feasibility of string-manipulating programs with complex operations. Proceedings of ACM Programming Languages, 3(POPL), 49:1\u201349:30. https:\/\/doi.org\/10.1145\/3290362","DOI":"10.1145\/3290362"},{"issue":"POPL","key":"9379_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3498707","volume":"6","author":"T Chen","year":"2022","unstructured":"Chen, T., Flores-Lamas, A., Hague, M., Han, Z., Hu, D., Kan, S., Lin, A. W., R\u00fcmmer, P., & Wu, Z. (2022). Solving string constraints with regex-dependent functions through transducers with priorities and variables. Proceedings of ACM Programming Languages, 6(POPL), 1\u201331. https:\/\/doi.org\/10.1145\/3498707","journal-title":"Proceedings of ACM Programming Languages"},{"key":"9379_CR25","doi-asserted-by":"publisher","unstructured":"Chen, T., Hague, M., He, J., Hu, D., Lin, A.\u00a0W., R\u00fcmmer, P., & Wu, Z. (2020). A decision procedure for path feasibility of string manipulating programs with integer data type. In D.\u00a0V. Hung, & O.\u00a0Sokolsky (Eds.), Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings, Vol. 12302 of Lecture Notes in Computer Science (pp. 325\u2013342). Springer. https:\/\/doi.org\/10.1007\/978-3-030-59152-6_18","DOI":"10.1007\/978-3-030-59152-6_18"},{"key":"9379_CR26","doi-asserted-by":"publisher","unstructured":"Abdulla, P.\u00a0A., Atig, M.\u00a0F., Diep, B.\u00a0P., Hol\u00edk, L., & Janku, P. (2019). Chain-free string constraints. In Y.\u00a0Chen, C.\u00a0Cheng, & J.\u00a0Esparza (Eds.), Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings, Vol. 11781 of Lecture Notes in Computer Science (pp. 277\u2013293). Springer. https:\/\/doi.org\/10.1007\/978-3-030-31784-3_16","DOI":"10.1007\/978-3-030-31784-3_16"},{"key":"9379_CR27","doi-asserted-by":"publisher","unstructured":"Abdulla, P.\u00a0A., Atig, M.\u00a0F., Chen, Y., Diep, B.\u00a0P., Hol\u00edk, L., Rezine, A., & R\u00fcmmer, P. (2018). Trau: SMT solver for string constraints. In N.\u00a0S. Bj\u00f8rner, & A.\u00a0Gurfinkel (Eds.), 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018 (pp. 1\u20135). IEEE. https:\/\/doi.org\/10.23919\/FMCAD.2018.8602997","DOI":"10.23919\/FMCAD.2018.8602997"},{"key":"9379_CR28","doi-asserted-by":"publisher","unstructured":"Abdulla, P.\u00a0A., Atig, M.\u00a0F., Chen, Y., Diep, B.\u00a0P., Hol\u00edk, L., Rezine, A., & R\u00fcmmer, P. (2017). Flatten and conquer: a framework for efficient analysis of string constraints. In A.\u00a0Cohen, & M.\u00a0T. Vechev (Eds.), Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017 (pp. 602\u2013617). ACM. https:\/\/doi.org\/10.1145\/3062341.3062384","DOI":"10.1145\/3062341.3062384"},{"key":"9379_CR29","doi-asserted-by":"publisher","unstructured":"Abdulla, P.\u00a0A., Atig, M.\u00a0F., Chen, Y., Diep, B.\u00a0P., Hol\u00edk, L., Hu, D., Tsai, W., Wu, Z., & Yen, D. (2021). Solving not-substring constraint with flat abstraction. In H.\u00a0Oh (Ed.), Programming Languages and Systems - 19th Asian Symposium, APLAS 2021, Chicago, IL, USA, October 17-18, 2021, Proceedings, Vol. 13008 of Lecture Notes in Computer Science (pp. 305\u2013320). Springer. https:\/\/doi.org\/10.1007\/978-3-030-89051-3_17","DOI":"10.1007\/978-3-030-89051-3_17"},{"key":"9379_CR30","doi-asserted-by":"publisher","unstructured":"Abdulla, P.\u00a0A., Atig, M.\u00a0F., Chen, Y., Hol\u00edk, L., Rezine, A., R\u00fcmmer, P., & Stenman, J. (2014). String constraints for verification. In A.\u00a0Biere, & R.\u00a0Bloem (Eds.), 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, Vol. 8559 of Lecture Notes in Computer Science (pp. 150\u2013166). Springer. https:\/\/doi.org\/10.1007\/978-3-319-08867-9_10","DOI":"10.1007\/978-3-319-08867-9_10"},{"key":"9379_CR31","doi-asserted-by":"publisher","unstructured":"Abdulla, P.\u00a0A., Atig, M.\u00a0F., Chen, Y., Hol\u00edk, L., Rezine, A., R\u00fcmmer, P., & Stenman, J. (2015). Norn: An SMT solver for string constraints. In D.\u00a0Kroening, & C.\u00a0S. Pasareanu (Eds.), Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, Vol. 9206 of Lecture Notes in Computer Science (pp. 462\u2013469). Springer. https:\/\/doi.org\/10.1007\/978-3-319-21690-4_29","DOI":"10.1007\/978-3-319-21690-4_29"},{"key":"9379_CR32","doi-asserted-by":"crossref","unstructured":"Trinh, M., Chu, D., & Jaffar, J. (2014). S3: A symbolic string solver for vulnerability detection in web applications. In CCS, ACM Transactions on Computational Logic (pp. 1232\u20131243).","DOI":"10.1145\/2660267.2660372"},{"key":"9379_CR33","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-030-02768-1_19","volume-title":"Programming Languages and Systems","author":"QL Le","year":"2018","unstructured":"Le, Q. L., & He, M. (2018). A decision procedure for string logic with quadratic equations, regular expressions and length constraints. In S. Ryu (Ed.), Programming Languages and Systems (pp. 350\u2013372). Cham: Springer International Publishing."},{"key":"9379_CR34","doi-asserted-by":"publisher","unstructured":"Abdulla, P.\u00a0A., Atig, M.\u00a0F., Chen, Y., Diep, B.\u00a0P., Dolby, J., Janku, P., Lin, H., Hol\u00edk, L., & Wu, W. (2020). Efficient handling of string-number conversion. In Proceedings of PLDI\u201920 (pp. 943\u2013957). ACM. https:\/\/doi.org\/10.1145\/3385412.3386034","DOI":"10.1145\/3385412.3386034"},{"key":"9379_CR35","doi-asserted-by":"crossref","unstructured":"Wang, H., Tsai, T., Lin, C., Yu, F., & Jiang, J.\u00a0R. (2016). String analysis via automata manipulation with logic circuit representation. In CAV\u201916, Vol. 9779 of LNCS (pp. 241\u2013260). Springer.","DOI":"10.1007\/978-3-319-41528-4_13"},{"key":"9379_CR36","doi-asserted-by":"publisher","unstructured":"Wang, H.-E., Chen, S.-Y., Yu, F., & Jiang, J.-H.\u00a0R. (2018). A symbolic model checking approach to the analysis of string and length constraints. In Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering, ASE 2018, Association for Computing Machinery, New York, NY, USA (pp. 623-633). https:\/\/doi.org\/10.1145\/3238147.3238189","DOI":"10.1145\/3238147.3238189"},{"issue":"4","key":"9379_CR37","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/s10515-012-0111-x","volume":"19","author":"P Hooimeijer","year":"2012","unstructured":"Hooimeijer, P., & Weimer, W. (2012). StrSolve: Solving string constraints lazily. Automated Software Engineering, 19(4), 531\u2013559.","journal-title":"Automated Software Engineering"},{"key":"9379_CR38","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-66158-2_1","volume-title":"Principles and Practice of Constraint Programming","author":"R Amadini","year":"2017","unstructured":"Amadini, R., Gange, G., Stuckey, P. J., & Tack, G. (2017). A novel approach to string constraint solving. In J. C. Beck (Ed.), Principles and Practice of Constraint Programming (pp. 3\u201320). Cham: Springer International Publishing."},{"key":"9379_CR39","doi-asserted-by":"crossref","unstructured":"Yu, F., Alkhalaf, M., & Bultan, T. (2010). Stranger: An automata-based string analysis tool for PHP. In TACAS\u201910, Vol. 6015 of LNCS (pp. 154\u2013157). Springer.","DOI":"10.1007\/978-3-642-12002-2_13"},{"issue":"1","key":"9379_CR40","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/s10703-013-0189-1","volume":"44","author":"F Yu","year":"2014","unstructured":"Yu, F., Alkhalaf, M., Bultan, T., & Ibarra, O. H. (2014). Automata-based symbolic string analysis for vulnerability detection. Formal Methods in System Design, 44(1), 44\u201370.","journal-title":"Formal Methods in System Design"},{"issue":"8","key":"9379_CR41","doi-asserted-by":"publisher","first-page":"1909","DOI":"10.1142\/S0129054111009112","volume":"22","author":"F Yu","year":"2011","unstructured":"Yu, F., Bultan, T., & Ibarra, O. H. (2011). Relational string verification using multi-track automata. International Journal of Foundations of Computer Science, 22(8), 1909\u20131924.","journal-title":"International Journal of Foundations of Computer Science"},{"key":"9379_CR42","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-319-21690-4_15","volume-title":"Computer Aided Verification","author":"A Aydin","year":"2015","unstructured":"Aydin, A., Bang, L., & Bultan, T. (2015). Automata-based model counting for string constraints. In D. Kroening & C. S. P\u0103s\u0103reanu (Eds.), Computer Aided Verification (pp. 255\u2013272). Cham: Springer International Publishing."},{"key":"9379_CR43","unstructured":"Bultan, T. (2025). contributors, ABC string solver. https:\/\/github.com\/vlab-cs-ucsb\/ABC"},{"key":"9379_CR44","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-319-59776-8_5","volume-title":"Integration of AI and OR Techniques in Constraint Programming","author":"JD Scott","year":"2017","unstructured":"Scott, J. D., Flener, P., Pearson, J., & Schulte, C. (2017). Design and implementation of bounded-length sequence variables. In D. Salvagnin & M. Lombardi (Eds.), Integration of AI and OR Techniques in Constraint Programming (pp. 51\u201367). Cham: Springer International Publishing."},{"issue":"4","key":"9379_CR45","first-page":"25:1","volume":"21","author":"A Kiezun","year":"2012","unstructured":"Kiezun, A., Ganesh, V., Artzi, S., Guo, P. J., Hooimeijer, P., & Ernst, M. D. (2012). HAMPI: A solver for word equations over strings, regular expressions, and context-free grammars. ACM Transactions on Computational Logic, 21(4), 25:1-25:28.","journal-title":"ACM Transactions on Computational Logic"},{"key":"9379_CR46","doi-asserted-by":"crossref","unstructured":"Saxena, P., Akhawe, D., Hanna, S., Mao, F., McCamant, S., & Song, D. (2010). A symbolic execution framework for JavaScript. In SP\u201910 (pp. 513\u2013528). IEEE Computer Society.","DOI":"10.1109\/SP.2010.38"},{"key":"9379_CR47","unstructured":"Cox, A., & Leasure, J. (2017). Model checking regular language constraints. CoRR abs\/1708.09073."},{"key":"9379_CR48","doi-asserted-by":"publisher","unstructured":"Chen, Y., Havlena, V., Leng\u00e1l, O., & Turrini, A. (2020). A symbolic algorithm for the case-split rule in string constraint solving. In B.\u00a0C. d.\u00a0S.\u00a0Oliveira (Ed.), Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Fukuoka, Japan, November 30 - December 2, 2020, Proceedings, Vol. 12470 of Lecture Notes in Computer Science (pp. 343\u2013363). Springer. https:\/\/doi.org\/10.1007\/978-3-030-64437-6_18","DOI":"10.1007\/978-3-030-64437-6_18"},{"key":"9379_CR49","doi-asserted-by":"publisher","unstructured":"Day, J.\u00a0D., Ehlers, T., Kulczynski, M., Manea, F., Nowotka, D., & Poulsen, D.\u00a0B. (2019). On solving word equations using SAT. In E.\u00a0Filiot, R.\u00a0M. Jungers, & I.\u00a0Potapov (Eds.), Reachability Problems - 13th International Conference, RP 2019, Brussels, Belgium, September 11-13, 2019, Proceedings, Vol. 11674 of Lecture Notes in Computer Science (pp. 93\u2013106). Springer. https:\/\/doi.org\/10.1007\/978-3-030-30806-3_8","DOI":"10.1007\/978-3-030-30806-3_8"},{"key":"9379_CR50","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-319-03077-7_2","volume-title":"Hardware and Software: Verification and Testing","author":"G Li","year":"2013","unstructured":"Li, G., & Ghosh, I. (2013). Pass: String solving with parameterized array and interval automaton. In V. Bertacco & A. Legay (Eds.), Hardware and Software: Verification and Testing (pp. 15\u201331). Cham: Springer International Publishing."},{"key":"9379_CR51","unstructured":"Hooimeijer, P., Livshits, B., Molnar, D., Saxena, P., & Veanes, M. (2011). Fast and precise sanitizer analysis with BEK. In USENIX Security Symposium 2011, USENIX Association."},{"key":"9379_CR52","doi-asserted-by":"crossref","unstructured":"Veanes, M., Hooimeijer, P., Livshits, B., Molnar, D., & Bj\u00f8rner, N. (2012). Symbolic finite state transducers: Algorithms and applications. In POPL\u201912, ACM Transactions on Computational Logic (pp. 137\u2013150).","DOI":"10.1145\/2103656.2103674"},{"key":"9379_CR53","unstructured":"Fu, X., & Li, C. (2010). Modeling regular replacement for string constraint solving. In NFM\u201910, Vol. NASA\/CP-2010-216215 of NASA (pp. 67\u201376)."},{"key":"9379_CR54","doi-asserted-by":"crossref","unstructured":"Trinh, M., Chu, D., & Jaffar, J. (2016). Progressive reasoning over recursively-defined strings. In CAV\u201916, Vol. 9779 of LNCS (pp. 218\u2013240). Springer.","DOI":"10.1007\/978-3-319-41528-4_12"},{"key":"9379_CR55","doi-asserted-by":"publisher","unstructured":"Day, J.\u00a0D., Ganesh, V., Grewal, N., & Manea, F. (2023). On the expressive power of string constraints. Proceedings of the ACM on Programming Languages 7(POPL). https:\/\/doi.org\/10.1145\/3571203","DOI":"10.1145\/3571203"},{"key":"9379_CR56","doi-asserted-by":"publisher","unstructured":"Plandowski, W. (1999). Satisfiability of word equations with constants is in NEXPTIME. In Proceedings of the Thirty-First Annual ACM Symposium on Theory of Computing, STOC \u201999, Association for Computing Machinery, New York, NY, USA (pp. 721\u2013725). https:\/\/doi.org\/10.1145\/301250.301443","DOI":"10.1145\/301250.301443"},{"key":"9379_CR57","doi-asserted-by":"publisher","unstructured":"Je\u017c, A. (2016). Recompression: A simple and powerful technique for word equations. Journal of ACM 63(1). https:\/\/doi.org\/10.1145\/2743014","DOI":"10.1145\/2743014"},{"key":"9379_CR58","doi-asserted-by":"crossref","unstructured":"Makanin, G. S. (1977). The problem of solvability of equations in a free semigroup. Matematicheskii Sbornik, 32(2), 147\u2013236. (in Russian).","DOI":"10.1070\/SM1977v032n02ABEH002376"},{"issue":"1","key":"9379_CR59","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/BF01457113","volume":"78","author":"J Nielsen","year":"1917","unstructured":"Nielsen, J. (1917). Die isomorphismen der allgemeinen, unendlichen gruppe mit zwei erzeugenden. Mathematische Annalen, 78(1), 385\u2013397.","journal-title":"Mathematische Annalen"},{"key":"9379_CR60","doi-asserted-by":"publisher","unstructured":"Blahoudek, F., Chen, Y., Chocholat\u00fd, D., Havlena, V., Hol\u00edk, L., Leng\u00e1l, O., & S\u00edc, J. (2023). Word equations in synergy with regular constraints. In M.\u00a0Chechik, J.\u00a0Katoen, & M.\u00a0Leucker (Eds.), Formal Methods - 25th International Symposium, FM 2023, L\u00fcbeck, Germany, March 6-10, 2023, Proceedings, Vol. 14000 of Lecture Notes in Computer Science (pp. 403\u2013423). Springer. https:\/\/doi.org\/10.1007\/978-3-031-27481-7_23","DOI":"10.1007\/978-3-031-27481-7_23"},{"key":"9379_CR61","unstructured":"Lentin, A. (1970). \u00c9quations dans les mono\u00efdes libres. Math\u00e9matiques et sciences humaines 31, 5\u201316. http:\/\/www.numdam.org\/item\/MSH_1970__31__5_0\/"},{"key":"9379_CR62","doi-asserted-by":"publisher","unstructured":"Choffrut, C., & Karhum\u00e4ki, J. (1997). Combinatorics of Words. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 329\u2013438. https:\/\/doi.org\/10.1007\/978-3-642-59136-5_6","DOI":"10.1007\/978-3-642-59136-5_6"},{"issue":"3","key":"9379_CR63","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1145\/337244.337255","volume":"47","author":"J Karhum\u00e4ki","year":"2000","unstructured":"Karhum\u00e4ki, J., Mignosi, F., & Plandowski, W. (2000). The expressibility of languages and relations by word equations. Journal of the ACM, 47(3), 483\u2013505. https:\/\/doi.org\/10.1145\/337244.337255","journal-title":"Journal of the ACM"},{"key":"9379_CR64","doi-asserted-by":"publisher","first-page":"731","DOI":"10.1007\/BFb0055097","volume-title":"Automata, Languages and Programming","author":"W Plandowski","year":"1998","unstructured":"Plandowski, W., & Rytter, W. (1998). Application of lempel-ziv encodings to the solution of word equations. In K. G. Larsen, S. Skyum, & G. Winskel (Eds.), Automata, Languages and Programming (pp. 731\u2013742). Berlin, Heidelberg: Springer Berlin Heidelberg."},{"key":"9379_CR65","doi-asserted-by":"publisher","unstructured":"Day, J.\u00a0D., Manea, F., & Nowotka, D. (2019). Upper bounds on the length of minimal solutions to certain quadratic word equations. In P.\u00a0Rossmanith, P.\u00a0Heggernes, J.-P., & Katoen (Eds.), 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019), Vol. 138 of Leibniz International Proceedings in Informatics (LIPIcs) (pp. 44:1\u201344:15). Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany. https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2019.44. https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.MFCS.2019.44","DOI":"10.4230\/LIPIcs.MFCS.2019.44"},{"key":"9379_CR66","unstructured":"Aziz, A., Singhal, V., Swamy, G., & Brayton, R.\u00a0K. (1993). Minimizing interacting finite state machines. Tech. Rep. UCB\/ERL M93\/68, EECS Department, University of California, Berkeley. http:\/\/www2.eecs.berkeley.edu\/Pubs\/TechRpts\/1993\/2425.html"},{"key":"9379_CR67","doi-asserted-by":"publisher","unstructured":"Henzinger, M., Henzinger, T., & Kopke, P. (1995). Computing simulations on finite and infinite graphs. In Proceedings of IEEE 36th Annual Foundations of Computer Science (pp. 453\u2013462). https:\/\/doi.org\/10.1109\/SFCS.1995.492576","DOI":"10.1109\/SFCS.1995.492576"},{"key":"9379_CR68","unstructured":"Blahoudek, F., Chen, Y.-F., Chocholat\u00fd, D., Havlena, V., Hol\u00edk, L., Leng\u00e1l, O., & S\u00ed\u010d, J. (2022). Noodler. https:\/\/github.com\/vhavlena\/Noodler"},{"key":"9379_CR69","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-031-57249-4_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Chocholat\u00fd","year":"2024","unstructured":"Chocholat\u00fd, D., Fiedor, T., Havlena, V., Hol\u00edk, L., Hru\u0161ka, M., Leng\u00e1l, O., & S\u00ed\u010d, J. (2024). Mata: A fast and simple finite automata library. In B. Finkbeiner & L. Kov\u00e1cs (Eds.), Tools and Algorithms for the Construction and Analysis of Systems (pp. 130\u2013151). Cham: Springer Nature Switzerland."},{"key":"9379_CR70","doi-asserted-by":"publisher","unstructured":"Lu, Z., Siemer, S., Jha, P., Day, J., Manea, F., & Ganesh, V. (2024). Layered and staged monte carlo tree search for smt strategy synthesis. In K.\u00a0Larson (Ed.), Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI-24 (pp. 1907\u20131915). International Joint Conferences on Artificial Intelligence Organization. main Track. https:\/\/doi.org\/10.24963\/ijcai.2024\/211","DOI":"10.24963\/ijcai.2024\/211"},{"key":"9379_CR71","doi-asserted-by":"publisher","unstructured":"Christensen, A.\u00a0S., M\u00f8ller, A., & Schwartzbach, M.\u00a0I. (2003). Precise analysis of string expressions. In R.\u00a0Cousot (Ed.), Static Analysis, 10th International Symposium, SAS 2003, San Diego, CA, USA, June 11-13, 2003, Proceedings, Vol. 2694 of Lecture Notes in Computer Science (pp. 1\u201318). Springer. https:\/\/doi.org\/10.1007\/3-540-44898-5_1","DOI":"10.1007\/3-540-44898-5_1"},{"key":"9379_CR72","doi-asserted-by":"publisher","unstructured":"Ganesh, V., Minnes, M., Solar-Lezama, A., & Rinard, M.\u00a0C. (2012). Word equations with length constraints: What\u2019s decidable?. In A.\u00a0Biere, A.\u00a0Nahir, & T.\u00a0E.\u00a0J. Vos (Eds.), Hardware and Software: Verification and Testing - 8th International Haifa Verification Conference, HVC 2012, Haifa, Israel, November 6-8, 2012. Revised Selected Papers, Vol. 7857 of Lecture Notes in Computer Science (pp. 209\u2013226). Springer. https:\/\/doi.org\/10.1007\/978-3-642-39611-3_21","DOI":"10.1007\/978-3-642-39611-3_21"},{"key":"9379_CR73","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-319-63139-4_4","volume-title":"Logic-Based Program Synthesis and Transformation","author":"R Amadini","year":"2017","unstructured":"Amadini, R., Flener, P., Pearson, J., Scott, J. D., Stuckey, P. J., & Tack, G. (2017). Minizinc with strings. In M. V. Hermenegildo & P. Lopez-Garcia (Eds.), Logic-Based Program Synthesis and Transformation (pp. 59\u201375). Cham: Springer International Publishing."}],"container-title":["Constraints"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-025-09379-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10601-025-09379-w","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-025-09379-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T08:12:17Z","timestamp":1770970337000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10601-025-09379-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,21]]},"references-count":73,"journal-issue":{"issue":"1-4","published-print":{"date-parts":[[2025,12]]}},"alternative-id":["9379"],"URL":"https:\/\/doi.org\/10.1007\/s10601-025-09379-w","relation":{},"ISSN":["1383-7133","1572-9354"],"issn-type":[{"value":"1383-7133","type":"print"},{"value":"1572-9354","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,5,21]]},"assertion":[{"value":"22 April 2025","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 May 2025","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors have no relevant financial or non-financial interests to disclose.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}]}}