{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T14:56:59Z","timestamp":1770994619274,"version":"3.50.1"},"publisher-location":"Cham","reference-count":66,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031274800","type":"print"},{"value":"9783031274817","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-3-031-27481-7_23","type":"book-chapter","created":{"date-parts":[[2023,3,2]],"date-time":"2023-03-02T14:03:10Z","timestamp":1677765790000},"page":"403-423","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Word Equations in Synergy with Regular Constraints"],"prefix":"10.1007","author":[{"given":"Franti\u0161ek","family":"Blahoudek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yu-Fang","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Chocholat\u00fd","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vojt\u011bch","family":"Havlena","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ond\u0159ej","family":"Leng\u00e1l","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Juraj","family":"S\u00ed\u010d","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,3,3]]},"reference":[{"key":"23_CR1","unstructured":"OWASP: Top 10 (2013). https:\/\/www.owasp.org\/images\/f\/f8\/OWASP_Top_10_-_2013.pdf"},{"key":"23_CR2","unstructured":"OWASP: Top 10 (2017). https:\/\/owasp.org\/www-project-top-ten\/2017\/"},{"key":"23_CR3","unstructured":"OWASP: Top 10 (2021). https:\/\/owasp.org\/Top10\/"},{"key":"23_CR4","unstructured":"Hadarean, L.: String solving at Amazon (2019). Presented at MOSCA 2019. https:\/\/mosca19.github.io\/program\/index.html"},{"key":"23_CR5","doi-asserted-by":"publisher","unstructured":"Alt, L., Blicha, M., Hyv\u00e4rinen, A.E.J., Sharygina, N.: SolCMC: solidity compiler\u2019s model checker. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification (CAV 2022). LNCS, vol. 13371, pp. 325\u2013338. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_16","DOI":"10.1007\/978-3-031-13185-1_16"},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science","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.: A DPLL(T) theory solver for a theory of strings and regular expressions. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 646\u2013662. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_43"},{"issue":"3","key":"23_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.: An efficient SMT solver for string constraints. Form. Methods Syst. Des. 48(3), 206\u2013234 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0247-6","journal-title":"Form. Methods Syst. Des."},{"key":"23_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 2016, ACM Trans. Comput. Log., pp. 4\u20136 (2016)","DOI":"10.1145\/2898375.2898393"},{"key":"23_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-319-24246-0_9","volume-title":"Frontiers of Combining Systems","author":"T Liang","year":"2015","unstructured":"Liang, T., Tsiskaridze, N., Reynolds, A., Tinelli, C., Barrett, C.: A decision procedure for regular membership and length constraints over unbounded strings. In: Lutz, C., Ranise, S. (eds.) FroCoS 2015. LNCS (LNAI), vol. 9322, pp. 135\u2013150. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24246-0_9"},{"key":"23_CR10","series-title":"Lecture Notes in Computer Science","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.: Scaling up DPLL(T) string solvers using context-dependent simplification. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 453\u2013474. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_24"},{"key":"23_CR11","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/978-3-031-13188-2_11","volume-title":"Computer Aided Verification (CAV 2022)","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 (CAV 2022), pp. 205\u2013226. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_11"},{"key":"23_CR12","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)"},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","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., et al.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24"},{"key":"23_CR14","unstructured":"Bj\u00f8rner, N., Tillmann, N., Voronkov, A.: Path feasibility analysis for string-manipulating programs. In: Tools and Algorithms for the Construction and Analysis of Systems: 15th International Conference (TACAS 2009), Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS 2009), York, UK, 22\u201329 March 2009. Proceedings 15, pp. 307\u2013321. Springer, Heidelberg (2009)"},{"key":"23_CR15","series-title":"Lecture Notes in Computer Science","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.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"23_CR16","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 2013, ACM Trans. Comput. Log., pp. 114\u2013124 (2013)","DOI":"10.1145\/2491411.2491456"},{"key":"23_CR17","doi-asserted-by":"crossref","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)","DOI":"10.23919\/FMCAD.2017.8102241"},{"key":"23_CR18","unstructured":"Murphy, B.: Z3str4: a solver for theories over strings. PhD thesis (2021)"},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science","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.: Effective search-space pruning for solvers of string equations, regular expressions and length constraints. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 235\u2013254. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_14"},{"key":"23_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-030-81688-9_14","volume-title":"Computer Aided Verification","author":"M Berzish","year":"2021","unstructured":"Berzish, M., et al.: An SMT solver for regular expressions and linear arithmetic over string length. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 289\u2013312. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_14"},{"key":"23_CR21","doi-asserted-by":"crossref","unstructured":"Lin, A.W., Barcel\u00f3, P.: String solving with word equations and transducers: towards a logic for analysing mutation XSS. In: POPL 2016, ACM Trans. Comput. Log., pp. 123\u2013136 (2016)","DOI":"10.1145\/2914770.2837641"},{"key":"23_CR22","doi-asserted-by":"crossref","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)","DOI":"10.1145\/3158091"},{"key":"23_CR23","doi-asserted-by":"crossref","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)","DOI":"10.1145\/3290362"},{"key":"23_CR24","doi-asserted-by":"crossref","unstructured":"Chen, T., et al.: Solving string constraints with regex-dependent functions through transducers with priorities and variables. Proc. ACM Program. Lang. 6(POPL), 1\u201331 (2022)","DOI":"10.1145\/3498707"},{"key":"23_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-030-59152-6_18","volume-title":"Automated Technology for Verification and Analysis","author":"T Chen","year":"2020","unstructured":"Chen, T., et al.: A decision procedure for path feasibility of string manipulating programs with integer data type. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 325\u2013342. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_18"},{"key":"23_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-030-31784-3_16","volume-title":"Automated Technology for Verification and Analysis","author":"PA Abdulla","year":"2019","unstructured":"Abdulla, P.A., Atig, M.F., Diep, B.P., Hol\u00edk, L., Jank\u016f, P.: Chain-free string constraints. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 277\u2013293. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_16"},{"key":"23_CR27","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., et al.: TRAU: SMT solver for string constraints. In: Bj\u00f8rner, N.S., Gurfinkel, A. (eds.) 2018 Formal Methods in Computer Aided Design (FMCAD 2018), pp. 1\u20135. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8602997"},{"key":"23_CR28","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., et al.: Flatten and conquer: a framework for efficient analysis of string constraints. In: Cohen, A., Vechev, M.T. (eds.) Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017), pp. 602\u2013617, ACM (2017)","DOI":"10.1145\/3062341.3062384"},{"key":"23_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-030-89051-3_17","volume-title":"Programming Languages and Systems","author":"PA Abdulla","year":"2021","unstructured":"Abdulla, P.A., et al.: Solving not-substring constraint with flat abstraction. In: Oh, H. (ed.) APLAS 2021. LNCS, vol. 13008, pp. 305\u2013320. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-89051-3_17"},{"key":"23_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-319-08867-9_10","volume-title":"Computer Aided Verification","author":"PA Abdulla","year":"2014","unstructured":"Abdulla, P.A., et al.: String constraints for verification. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 150\u2013166. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_10"},{"key":"23_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-319-21690-4_29","volume-title":"Computer Aided Verification","author":"PA Abdulla","year":"2015","unstructured":"Abdulla, P.A., et al.: Norn: an SMT solver for string constraints. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 462\u2013469. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_29"},{"key":"23_CR32","doi-asserted-by":"crossref","unstructured":"Trinh, M., Chu, D., Jaffar, J.: S3: a symbolic string solver for vulnerability detection in web applications. In: CCS, ACM Trans. Comput. Log., pp. 1232\u20131243 (2014)","DOI":"10.1145\/2660267.2660372"},{"key":"23_CR33","series-title":"Lecture Notes in Computer Science","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.: A decision procedure for string logic with quadratic equations, regular expressions and length constraints. In: Ryu, S. (ed.) APLAS 2018. LNCS, vol. 11275, pp. 350\u2013372. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02768-1_19"},{"key":"23_CR34","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., et al.: Efficient handling of string-number conversion. In: Proc. of PLDI 2020, ACM, pp. 943\u2013957 (2020)","DOI":"10.1145\/3385412.3386034"},{"key":"23_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-319-41528-4_13","volume-title":"Computer Aided Verification","author":"H-E Wang","year":"2016","unstructured":"Wang, H.-E., Tsai, T.-L., Lin, C.-H., Yu, F., Jiang, J.-H.R.: String analysis via automata manipulation with logic circuit representation. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 241\u2013260. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_13"},{"key":"23_CR36","doi-asserted-by":"crossref","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 (ASE 2018), pp. 623\u2013633. Association for Computing Machinery, NY (2018)","DOI":"10.1145\/3238147.3238189"},{"issue":"4","key":"23_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.: StrSolve: solving string constraints lazily. Autom. Softw. Eng. 19(4), 531\u2013559 (2012)","journal-title":"Autom. Softw. Eng."},{"key":"23_CR38","series-title":"Lecture Notes in Computer Science","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.: A novel approach to string constraint solving. In: Beck, J.C. (ed.) CP 2017. LNCS, vol. 10416, pp. 3\u201320. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66158-2_1"},{"key":"23_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-642-12002-2_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Yu","year":"2010","unstructured":"Yu, F., Alkhalaf, M., Bultan, T.: Stranger: an automata-based string analysis tool for PHP. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 154\u2013157. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_13"},{"issue":"1","key":"23_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.: Automata-based symbolic string analysis for vulnerability detection. Form. Methods Syst. Des. 44(1), 44\u201370 (2014)","journal-title":"Form. Methods Syst. Des."},{"issue":"8","key":"23_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.: Relational string verification using multi-track automata. Int. J. Found. Comput. Sci. 22(8), 1909\u20131924 (2011)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"23_CR42","series-title":"Lecture Notes in Computer Science","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.: Automata-based model counting for string constraints. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 255\u2013272. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_15"},{"key":"23_CR43","unstructured":"Bultan, T., contributors: ABC string solver"},{"key":"23_CR44","series-title":"Lecture Notes in Computer Science","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.: Design and implementation of bounded-length sequence variables. In: Salvagnin, D., Lombardi, M. (eds.) CPAIOR 2017. LNCS, vol. 10335, pp. 51\u201367. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-59776-8_5"},{"key":"23_CR45","doi-asserted-by":"crossref","unstructured":"Kiezun, A., Ganesh, V., Artzi, S., Guo, P.J., Hooimeijer, P., Ernst, M.D.: HAMPI: a solver for word equations over strings, regular expressions, and context-free grammars. ACM Trans. Comput. Log. 21(4), 25:1\u201325:28 (2012)","DOI":"10.1145\/2377656.2377662"},{"key":"23_CR46","doi-asserted-by":"crossref","unstructured":"Saxena, P., Akhawe, D., Hanna, S., Mao, F., McCamant, S., Song, D.: A symbolic execution framework for JavaScript. In: SP 2010, IEEE Computer Society, pp. 513\u2013528 (2010)","DOI":"10.1109\/SP.2010.38"},{"key":"23_CR47","unstructured":"Cox, A., Leasure, J.: Model checking regular language constraints. arXiv preprint arXiv:1708.09073 (2017)"},{"key":"23_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-030-64437-6_18","volume-title":"Programming Languages and Systems","author":"Y-F Chen","year":"2020","unstructured":"Chen, Y.-F., Havlena, V., Leng\u00e1l, O., Turrini, A.: A symbolic algorithm for the case-split rule in string constraint solving. In: Oliveira, B.C.S. (ed.) APLAS 2020. LNCS, vol. 12470, pp. 343\u2013363. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-64437-6_18"},{"key":"23_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-030-30806-3_8","volume-title":"Reachability Problems","author":"JD Day","year":"2019","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., Potapov, I. (eds.) RP 2019. LNCS, vol. 11674, pp. 93\u2013106. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30806-3_8"},{"key":"23_CR50","series-title":"Lecture Notes in Computer Science","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.: PASS: string solving with parameterized array and interval automaton. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol. 8244, pp. 15\u201331. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-03077-7_2"},{"key":"23_CR51","unstructured":"Hooimeijer, P., Livshits, B., Molnar, D., Saxena, P., Veanes, M.: Fast and precise sanitizer analysis with BEK. In: USENIX Security Symposium 2011, USENIX Association (2011)"},{"key":"23_CR52","doi-asserted-by":"crossref","unstructured":"Veanes, M., Hooimeijer, P., Livshits, B., Molnar, D., Bj\u00f8rner, N.: Symbolic finite state transducers: algorithms and applications. In: POPL 2012, ACM Trans. Comput. Log., pp. 137\u2013150 (2012)","DOI":"10.1145\/2103621.2103674"},{"key":"23_CR53","unstructured":"Fu, X., Li, C.: Modeling regular replacement for string constraint solving. In: NFM 2010. Volume NASA\/CP-2010-216215 of NASA, pp. 67\u201376 (2010)"},{"key":"23_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-319-41528-4_12","volume-title":"Computer Aided Verification","author":"M-T Trinh","year":"2016","unstructured":"Trinh, M.-T., Chu, D.-H., Jaffar, J.: Progressive reasoning over recursively-defined strings. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 218\u2013240. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_12"},{"key":"23_CR55","doi-asserted-by":"crossref","unstructured":"Plandowski, W.: Satisfiability of word equations with constants is in NEXPTIME. In: Proceedings of the Thirty-First Annual ACM Symposium on Theory of Computing (STOC 1999), pp. 721\u2013725. Association for Computing Machinery, NY (1999)","DOI":"10.1145\/301250.301443"},{"issue":"1","key":"23_CR56","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2743014","volume":"63","author":"A Je\u017c","year":"2016","unstructured":"Je\u017c, A.: Recompression: a simple and powerful technique for word equations. J. ACM 63(1), 1\u201351 (2016)","journal-title":"J. ACM"},{"issue":"2","key":"23_CR57","first-page":"147","volume":"32","author":"GS Makanin","year":"1977","unstructured":"Makanin, G.S.: The problem of solvability of equations in a free semigroup. Matematicheskii Sbornik 32(2), 147\u2013236 (1977). (in Russian)","journal-title":"Matematicheskii Sbornik"},{"issue":"1","key":"23_CR58","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/BF01457113","volume":"78","author":"J Nielsen","year":"1917","unstructured":"Nielsen, J.: Die isomorphismen der allgemeinen, unendlichen gruppe mit zwei erzeugenden. Math. Ann. 78(1), 385\u2013397 (1917)","journal-title":"Math. Ann."},{"key":"23_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-39611-3_21","volume-title":"Hardware and Software: Verification and Testing","author":"V Ganesh","year":"2013","unstructured":"Ganesh, V., Minnes, M., Solar-Lezama, A., Rinard, M.: Word equations with length constraints: what\u2019s decidable? In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 209\u2013226. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39611-3_21"},{"key":"23_CR60","unstructured":"Blahoudek, F., et al.: Word equations in synergy with regular constraints (technical report). arXiv preprint arXiv:2212.02317 (2022)"},{"key":"23_CR61","unstructured":"Aziz, A., Singhal, V., Swamy, G., Brayton, R.K.: Minimizing interacting finite state machines. Technical Report UCB\/ERL M93\/68, EECS Department, University of California, Berkeley (1993)"},{"key":"23_CR62","doi-asserted-by":"crossref","unstructured":"Henzinger, M., Henzinger, T., Kopke, P.: Computing simulations on finite and infinite graphs. In: Proceedings of IEEE 36th Annual Foundations of Computer Science, pp. 453\u2013462 (1995)","DOI":"10.1109\/SFCS.1995.492576"},{"key":"23_CR63","unstructured":"Blahoudek, F., et al.: Noodler (2022). https:\/\/github.com\/vhavlena\/Noodler"},{"key":"23_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-030-90870-6_21","volume-title":"Formal Methods","author":"F Mora","year":"2021","unstructured":"Mora, F., Berzish, M., Kulczynski, M., Nowotka, D., Ganesh, V.: Z3str4: a multi-armed string solver. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 389\u2013406. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_21"},{"key":"23_CR65","doi-asserted-by":"crossref","unstructured":"Hol\u00edk, L., Janku, P., Lin, A.W., R\u00fcmmer, P., Vojnar, T.: String constraints with concatenation and transducers solved efficiently. Proc. ACM Program. Lang. 2(POPL), 4:1\u20134:32 (2018)","DOI":"10.1145\/3158092"},{"key":"23_CR66","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44898-5_1","volume-title":"Static Analysis","author":"AS Christensen","year":"2003","unstructured":"Christensen, A.S., M\u00f8ller, A., Schwartzbach, M.I.: Precise analysis of string expressions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 1\u201318. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-44898-5_1"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-27481-7_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,15]],"date-time":"2024-10-15T16:25:05Z","timestamp":1729009505000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-27481-7_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031274800","9783031274817"],"references-count":66,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-27481-7_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"3 March 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"L\u00fcbeck","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 March 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 March 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/fm2023.isp.uni-luebeck.de\/wordpress\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"95","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"27% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The proceedings also include 7 short industry papers","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}