{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:43:19Z","timestamp":1764402199267,"version":"3.46.0"},"publisher-location":"Cham","reference-count":57,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031906527"},{"type":"electronic","value":"9783031906534"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    <jats:sc>Z3-Noodler<\/jats:sc>\n                    is a fork of the\n                    <jats:sc>Z3<\/jats:sc>\n                    SMT solver replacing its string theory implementation with a\u00a0portfolio of decision procedures and a\u00a0selection mechanism\u00a0for choosing among them based on the features of the input formula. In this paper, we give an overview of the used decision procedures, including a\u00a0novel length-based procedure, and their integration into a\u00a0robust solver with a\u00a0good overall performance, as witnessed by\n                    <jats:sc>Z3-Noodler<\/jats:sc>\n                    winning the string division of SMT-COMP\u201924 by a\u00a0large margin. We also extended the solver with a\u00a0support for model generation, which\u00a0is essential for the use of the solver in practice.\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-90653-4_2","type":"book-chapter","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T08:39:35Z","timestamp":1746175175000},"page":"23-44","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-5614-1592","authenticated-orcid":false,"given":"David","family":"Chocholat\u00fd","sequence":"first","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\/0009-0007-5496-0057","authenticated-orcid":false,"given":"Jan","family":"Hrani\u010dka","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,1]]},"reference":[{"key":"2_CR1","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: Biere, A., Bloem, R. (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. 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"},{"key":"2_CR2","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y., Hol\u00edk, L., Rezine, A., R\u00fcmmer, P., Stenman, J.: Norn: An SMT solver for string constraints. In: Kroening, D., Pasareanu, C.S. (eds.) Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. Lecture Notes in Computer Science, vol.\u00a09206, pp. 462\u2013469. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_29, https:\/\/doi.org\/10.1007\/978-3-319-21690-4_29","DOI":"10.1007\/978-3-319-21690-4_29"},{"key":"2_CR3","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Diep, B.P., Hol\u00edk, L., Jank\u016f, P.: Chain-free string constraints. In: Chen, Y., Cheng, C., Esparza, J. (eds.) Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11781, pp. 277\u2013293. Springer (2019).https:\/\/doi.org\/10.1007\/978-3-030-31784-3_16, https:\/\/doi.org\/10.1007\/978-3-030-31784-3_16","DOI":"10.1007\/978-3-030-31784-3_16"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Chen, Y.F., Hol\u00edk, L., Mayr, R., Vojnar, T.: When simulation meets antichains. In: TACAS\u201910. LNCS, vol.\u00a06015, pp. 158\u2013174. Springer (2010)","DOI":"10.1007\/978-3-642-12002-2_14"},{"key":"2_CR5","doi-asserted-by":"publisher","unstructured":"Backes, J., Bolignano, P., Cook, B., Dodge, C., Gacek, A., Luckow, K., Rungta, N., Tkachuk, O., Varming, C.: Semantic-based automated reasoning for aws access policies using smt. In: 2018 Formal Methods in Computer Aided Design (FMCAD). pp.\u00a01\u20139 (2018).https:\/\/doi.org\/10.23919\/FMCAD.2018.8602994","DOI":"10.23919\/FMCAD.2018.8602994"},{"key":"2_CR6","doi-asserted-by":"crossref","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.: cvc5: A versatile and industrial-strength smt solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 415\u2013442. Springer International Publishing, Cham (2022)","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"2_CR7","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Barrett, C.W., Tinelli, C., Deters, M., Liang, T., Reynolds, A., Tsiskaridze, N.: Efficient solving of string constraints for security analysis. In: HotSoS\u201916. pp.\u00a04\u20136. ACM Trans. Comput. Log. (2016)","DOI":"10.1145\/2898375.2898393"},{"key":"2_CR9","unstructured":"Bernardo, P., Veronese, L., Valle, V.D., Calzavara, S., Squarcina, M., Ad\u00e3o, P., Maffei, M.: Web platform threats: Automated detection of web security issues with WPT. In: 33rd USENIX Security Symposium (USENIX Security 24). pp. 757\u2013774. USENIX Association, Philadelphia, PA (Aug 2024), https:\/\/www.usenix.org\/conference\/usenixsecurity24\/presentation\/bernardo"},{"key":"2_CR10","doi-asserted-by":"publisher","unstructured":"Berzish, M., Day, J.D., Ganesh, V., Kulczynski, M., Manea, F., Mora, F., Nowotka, D.: Towards more efficient methods for solving regular-expression heavy string constraints. Theor. Comput. Sci. 943, 50\u201372 (2023). https:\/\/doi.org\/10.1016\/j.tcs.2022.12.009, https:\/\/doi.org\/10.1016\/j.tcs.2022.12.009","DOI":"10.1016\/j.tcs.2022.12.009"},{"key":"2_CR11","doi-asserted-by":"publisher","unstructured":"Berzish, M., Ganesh, V., Zheng, Y.: Z3str3: A string solver with theory-aware heuristics. In: 2017 Formal Methods in Computer Aided Design (FMCAD). pp. 55\u201359 (2017).https:\/\/doi.org\/10.23919\/FMCAD.2017.8102241","DOI":"10.23919\/FMCAD.2017.8102241"},{"key":"2_CR12","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: Silva, A., Leino, K.R.M. (eds.) 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"},{"key":"2_CR13","unstructured":"Berzish, Murphy: Z3str4: A Solver for Theories over Strings. Ph.D. thesis (2021), http:\/\/hdl.handle.net\/10012\/17102"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., Tillmann, N., Voronkov, A.: Path feasibility analysis for string-manipulating programs. In: TACAS\u201909. LNCS, vol.\u00a05505, pp. 307\u2013321. Springer (2009)","DOI":"10.1007\/978-3-642-00768-2_27"},{"key":"2_CR15","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: Chechik, M., Katoen, J.P., Leucker, M. (eds.) Formal Methods. pp. 403\u2013423. Springer International Publishing, Cham (2023)","DOI":"10.1007\/978-3-031-27481-7_23"},{"key":"2_CR16","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 (technical report) (2022), an extended version of the paper published at FM\u201923","DOI":"10.1007\/978-3-031-27481-7_23"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Blotsky, D., Mora, F., Berzish, M., Zheng, Y., Kabir, I., Ganesh, V.: StringFuzz: A fuzzer for string solvers. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification. pp. 45\u201351. Springer International Publishing, Cham (2018)","DOI":"10.1007\/978-3-319-96142-2_6"},{"key":"2_CR18","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":"2_CR19","doi-asserted-by":"crossref","unstructured":"Bustan, D., Grumberg, O.: Simulation based minimization. In: Proceedings of CADE-17. LNCS, vol.\u00a01831, pp. 255\u2013270. Springer (2000)","DOI":"10.1007\/10721959_20"},{"key":"2_CR20","doi-asserted-by":"publisher","unstructured":"Chen, T., Chen, Y., Hague, M., Lin, A.W., Wu, Z.: What is decidable about string constraints with the replaceall function. Proc. ACM Program. Lang. 2(POPL), 3:1\u20133:29 (2018). https:\/\/doi.org\/10.1145\/3158091, https:\/\/doi.org\/10.1145\/3158091","DOI":"10.1145\/3158091"},{"key":"2_CR21","doi-asserted-by":"publisher","unstructured":"Chen, T., Flores-Lamas, A., Hague, M., Han, Z., Hu, D., Kan, S., Lin, A.W., R\u00fcmmer, P., Wu, Z.: Solving string constraints with regex-dependent functions through transducers with priorities and variables. Proc. ACM Program. Lang. 6(POPL), 1\u201331 (2022). https:\/\/doi.org\/10.1145\/3498707, https:\/\/doi.org\/10.1145\/3498707","DOI":"10.1145\/3498707"},{"key":"2_CR22","doi-asserted-by":"publisher","unstructured":"Chen, T., Hague, M., He, J., Hu, D., Lin, A.W., R\u00fcmmer, P., Wu, Z.: A decision procedure for path feasibility of string manipulating programs with integer data type. In: Hung, D.V., Sokolsky, O. (eds.) Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12302, pp. 325\u2013342. Springer (2020).https:\/\/doi.org\/10.1007\/978-3-030-59152-6_18, https:\/\/doi.org\/10.1007\/978-3-030-59152-6_18","DOI":"10.1007\/978-3-030-59152-6_18"},{"key":"2_CR23","doi-asserted-by":"publisher","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. ACM Program. Lang. 3(POPL), 49:1\u201349:30 (2019).https:\/\/doi.org\/10.1145\/3290362, https:\/\/doi.org\/10.1145\/3290362","DOI":"10.1145\/3290362"},{"key":"2_CR24","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: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 24\u201333. Springer Nature Switzerland, Cham (2024)","DOI":"10.1007\/978-3-031-57246-3_2"},{"key":"2_CR25","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":"2_CR26","doi-asserted-by":"crossref","unstructured":"Chocholat\u00fd, D., Fiedor, T., Havlena, V., Hol\u00edk, L., Hru\u0161ka, M., Leng\u00e1l, O., S\u00ed\u010d, J.: Mata: A fast and simple finite automata library. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 130\u2013151. Springer Nature Switzerland, Cham (2024)","DOI":"10.1007\/978-3-031-57249-4_7"},{"key":"2_CR27","doi-asserted-by":"publisher","unstructured":"Chocholat\u00fd, D., Havlena, V., Hol\u00edk, L., Leng\u00e1l, O., S\u00ed\u010d, J.: Z3-Noodler 1.3: Shepherding decision procedures for strings with model generation (Oct 2024).https:\/\/doi.org\/10.5281\/zenodo.13989789, https:\/\/doi.org\/10.5281\/zenodo.13989789","DOI":"10.5281\/zenodo.13989789"},{"key":"2_CR28","doi-asserted-by":"publisher","unstructured":"Day, J.D., Ehlers, T., Kulczynski, M., Manea, F., Nowotka, D., Poulsen, D.B.: On solving word equations using SAT. In: Filiot, E., Jungers, R.M., Potapov, I. (eds.) Reachability Problems - 13th International Conference, RP 2019, Brussels, Belgium, September 11-13, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11674, pp. 93\u2013106. Springer (2019).https:\/\/doi.org\/10.1007\/978-3-030-30806-3_8, https:\/\/doi.org\/10.1007\/978-3-030-30806-3_8","DOI":"10.1007\/978-3-030-30806-3_8"},{"key":"2_CR29","doi-asserted-by":"publisher","unstructured":"Havlena, V., Hol\u00edk, L., Leng\u00e1l, O., S\u00ed\u010d, J.: Cooking String-Integer Conversions with Noodles. In: Chakraborty, S., Jiang, J.H.R. (eds.) 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0305, pp. 14:1\u201314:19. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2024).https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2024.14, https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.SAT.2024.14","DOI":"10.4230\/LIPIcs.SAT.2024.14"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Le, Q.L., He, M.: A decision procedure for string logic with quadratic equations, regular expressions and length constraints. In: Ryu, S. (ed.) Programming Languages and Systems. pp. 350\u2013372. Springer International Publishing, Cham (2018)","DOI":"10.1007\/978-3-030-02768-1_19"},{"key":"2_CR31","unstructured":"Liana Hadarean: String solving at Amazon. https:\/\/mosca19.github.io\/program\/index.html (2019), presented at MOSCA\u201919"},{"key":"2_CR32","doi-asserted-by":"crossref","unstructured":"Liang, T., Reynolds, A., Tinelli, C., Barrett, C., Deters, M.: A DPLL(T) theory solver for a theory of strings and regular expressions. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification. pp. 646\u2013662. Springer International Publishing, Cham (2014)","DOI":"10.1007\/978-3-319-08867-9_43"},{"key":"2_CR33","doi-asserted-by":"crossref","unstructured":"Liang, T., Reynolds, A., Tsiskaridze, N., Tinelli, C., Barrett, C., Deters, M.: An efficient SMT solver for string constraints. Formal Methods in System Design 48(3), 206\u2013234 (2016)","DOI":"10.1007\/s10703-016-0247-6"},{"key":"2_CR34","doi-asserted-by":"crossref","unstructured":"Liang, T., Tsiskaridze, N., Reynolds, A., Tinelli, C., Barrett, C.: A decision procedure for regular membership and length constraints over unbounded strings. In: FroCoS\u201915. LNCS, vol.\u00a09322, pp. 135\u2013150. Springer (2015)","DOI":"10.1007\/978-3-319-24246-0_9"},{"key":"2_CR35","doi-asserted-by":"publisher","unstructured":"Lin, A.W., Majumdar, R.: Quadratic word equations with length constraints, counter systems, and presburger arithmetic with divisibility. Log. Methods Comput. Sci. 17(4) (2021).https:\/\/doi.org\/10.46298\/lmcs-17(4:4)2021, https:\/\/doi.org\/10.46298\/lmcs-17(4:4)2021","DOI":"10.46298\/lmcs-17(4:4)2021"},{"key":"2_CR36","doi-asserted-by":"publisher","unstructured":"Lin, A.W., Barcel\u00f3, P.: String solving with word equations and transducers: towards a logic for analysing mutation XSS. In: Bod\u00edk, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016. pp. 123\u2013136. ACM (2016). https:\/\/doi.org\/10.1145\/2837614.2837641, https:\/\/doi.org\/10.1145\/2837614.2837641","DOI":"10.1145\/2837614.2837641"},{"key":"2_CR37","doi-asserted-by":"publisher","unstructured":"Loring, B., Mitchell, D., Kinder, J.: Sound regular expression semantics for dynamic symbolic execution of javascript. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. p. 425-438. PLDI 2019, Association for Computing Machinery, New York, NY, USA (2019).https:\/\/doi.org\/10.1145\/3314221.3314645, https:\/\/doi.org\/10.1145\/3314221.3314645","DOI":"10.1145\/3314221.3314645"},{"key":"2_CR38","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: TACAS\u201908. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer (2008), https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"2_CR39","doi-asserted-by":"crossref","unstructured":"Nielsen, J.: Die isomorphismen der allgemeinen, unendlichen gruppe mit zwei erzeugenden. Mathematische Annalen 78(1), 385\u2013397 (1917)","DOI":"10.1007\/BF01457113"},{"key":"2_CR40","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.: Even faster conflicts and lazier reductions for string solvers. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification. pp. 205\u2013226. Springer International Publishing, Cham (2022)"},{"key":"2_CR41","doi-asserted-by":"crossref","unstructured":"N\u00f6tzli, A., Reynolds, A., Barbosa, H., Niemetz, A., Preiner, M., Barrett, C., Tinelli, C.: Syntax-guided rewrite rule enumeration for SMT solvers. In: Janota, M., Lynce, I. (eds.) Theory and Applications of Satisfiability Testing \u2013 SAT 2019. pp. 279\u2013297. Springer International Publishing, Cham (2019)","DOI":"10.1007\/978-3-030-24258-9_20"},{"key":"2_CR42","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Notzlit, A., Barrett, C., Tinelli, C.: Reductions for strings and regular expressions revisited. In: 2020 Formal Methods in Computer Aided Design (FMCAD). pp. 225\u2013235 (2020).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":"2_CR43","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Woo, M., Barrett, C., Brumley, D., Liang, T., Tinelli, C.: Scaling up DPLL(T) string solvers using context-dependent simplification. In: Majumdar, R., Kun\u010dak, V. (eds.) Computer Aided Verification. pp. 453\u2013474. Springer International Publishing, Cham (2017)","DOI":"10.1007\/978-3-319-63390-9_24"},{"key":"2_CR44","doi-asserted-by":"publisher","unstructured":"Rungta, N.: A billion SMT queries a day (invited paper). In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I. Lecture Notes in Computer Science, vol. 13371, pp. 3\u201318. Springer (2022).https:\/\/doi.org\/10.1007\/978-3-031-13185-1_1, https:\/\/doi.org\/10.1007\/978-3-031-13185-1_1","DOI":"10.1007\/978-3-031-13185-1_1"},{"key":"2_CR45","doi-asserted-by":"crossref","unstructured":"Saxena, P., Akhawe, D., Hanna, S., Mao, F., McCamant, S., Song, D.: A symbolic execution framework for javascript. In: 2010 IEEE Symposium on Security and Privacy. pp. 513\u2013528. IEEE (2010)","DOI":"10.1109\/SP.2010.38"},{"key":"2_CR46","unstructured":"Saxena, P., Akhawe, D., Hanna, S., Mao, F., McCamant, S., Song, D.: Kaluza web site (2023), https:\/\/webblaze.cs.berkeley.edu\/2010\/kaluza\/"},{"key":"2_CR47","unstructured":"SMT-COMP\u201924: https:\/\/smt-comp.github.io\/2024\/ (2024)"},{"key":"2_CR48","doi-asserted-by":"publisher","unstructured":"Stanford, C., Veanes, M., Bj\u00f8rner, N.: Symbolic boolean derivatives for efficiently solving extended regular expression constraints. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. p. 620-635. PLDI 2021, Association for Computing Machinery, New York, NY, USA (2021).https:\/\/doi.org\/10.1145\/3453483.3454066, https:\/\/doi.org\/10.1145\/3453483.3454066","DOI":"10.1145\/3453483.3454066"},{"key":"2_CR49","doi-asserted-by":"crossref","unstructured":"Trinh, M., Chu, D., Jaffar, J.: S3: A symbolic string solver for vulnerability detection in web applications. In: CCS. pp. 1232\u20131243. ACM Trans. Comput. Log. (2014)","DOI":"10.1145\/2660267.2660372"},{"key":"2_CR50","doi-asserted-by":"crossref","unstructured":"Trinh, M., Chu, D., Jaffar, J.: progressive reasoning over recursively-defined strings. In: CAV\u201916. LNCS, vol.\u00a09779, pp. 218\u2013240. Springer (2016)","DOI":"10.1007\/978-3-319-41528-4_12"},{"key":"2_CR51","doi-asserted-by":"publisher","unstructured":"Trinh, M.T., Chu, D.H., Jaffar, J.: Inter-theory dependency analysis for smt string solvers. Proc. ACM Program. Lang. 4(OOPSLA) (Nov 2020).https:\/\/doi.org\/10.1145\/3428260, https:\/\/doi.org\/10.1145\/3428260","DOI":"10.1145\/3428260"},{"key":"2_CR52","doi-asserted-by":"publisher","unstructured":"Wang, H.E., Chen, S.Y., Yu, F., Jiang, J.H.R.: 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. p. 623-633. ASE 2018, Association for Computing Machinery, New York, NY, USA (2018).https:\/\/doi.org\/10.1145\/3238147.3238189, https:\/\/doi.org\/10.1145\/3238147.3238189","DOI":"10.1145\/3238147.3238189"},{"key":"2_CR53","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: CAV\u201916. LNCS, vol.\u00a09779, pp. 241\u2013260. Springer (2016)","DOI":"10.1007\/978-3-319-41528-4_13"},{"key":"2_CR54","doi-asserted-by":"crossref","unstructured":"Wulf, M.D., Doyen, L., Henzinger, T.A., Raskin, J.: Antichains: A new algorithm for checking universality of finite automata. In: CAV\u201906. LNCS, vol.\u00a04144, pp. 17\u201330. Springer (2006)","DOI":"10.1007\/11817963_5"},{"key":"2_CR55","doi-asserted-by":"crossref","unstructured":"Yu, F., Alkhalaf, M., Bultan, T., Ibarra, O.H.: Automata-based symbolic string analysis for vulnerability detection. Formal Methods in System Design 44(1), 44\u201370 (2014)","DOI":"10.1007\/s10703-013-0189-1"},{"key":"2_CR56","doi-asserted-by":"crossref","unstructured":"Zheng, Y., Ganesh, V., Subramanian, S., Tripp, O., Dolby, J., Zhang, X.: Effective search-space pruning for solvers of string equations, regular expressions and length constraints. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) Computer Aided Verification. pp. 235\u2013254. Springer International Publishing, Cham (2015)","DOI":"10.1007\/978-3-319-21690-4_14"},{"key":"2_CR57","doi-asserted-by":"crossref","unstructured":"Zheng, Y., Zhang, X., Ganesh, V.: Z3-str: A Z3-based string solver for web application analysis. In: ESEC\/FSE\u201913. pp. 114\u2013124. ACM Trans. Comput. Log. (2013)","DOI":"10.1145\/2491411.2491456"}],"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-90653-4_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:36:40Z","timestamp":1764401800000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90653-4_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906527","9783031906534"],"references-count":57,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90653-4_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","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":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}