{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T09:06:01Z","timestamp":1784797561111,"version":"3.55.0"},"publisher-location":"Cham","reference-count":49,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325259","type":"print"},{"value":"9783032325266","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We generalize an efficient automata-based approach to string solving, the\n                    <jats:italic>stabilization-based<\/jats:italic>\n                    method behind the solver\n                    <jats:sc>Z3-Noodler<\/jats:sc>\n                    , to support relational constraints represented by finite-state transducers (useful for modeling  constraints, etc.). We focus on efficient handling of length constraints by reducing the need for expensive concatenation elimination, a major bottleneck in automata-based string solving. We also propose heuristics that significantly improve performance in practice. Implemented on top of\n                    <jats:sc>Z3-Noodler<\/jats:sc>\n                    , our method clearly outperforms other solvers on benchmarks with relational constraints: it solves more instances and runs orders of magnitude faster.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32526-6_3","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:45:20Z","timestamp":1784796320000},"page":"50-74","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["String Solving with\u00a0Stabilization and\u00a0Transducers"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-5614-1592","authenticated-orcid":false,"given":"David","family":"Chocholat\u00fd","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4375-7954","authenticated-orcid":false,"given":"Vojt\u011bch","family":"Havlena","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6957-1651","authenticated-orcid":false,"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7454-3751","authenticated-orcid":false,"given":"Juraj","family":"S\u00ed\u010d","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-0091-0546","authenticated-orcid":false,"given":"Michal","family":"\u0160ed\u00fd","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"3_CR1","unstructured":"SMT-COMP QF_Strings, 2024 (2024). https:\/\/smt-comp.github.io\/2024\/results\/qf_strings-single-query\/"},{"key":"3_CR2","unstructured":"SMT-COMP QF_Strings, 2025 (2025). https:\/\/smt-comp.github.io\/2025\/results\/qf_slia-single-query\/"},{"key":"3_CR3","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., et\u00a0al.: 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, Barcelona, Spain, June 18-23, 2017, pp. 602\u2013617. ACM (2017). https:\/\/doi.org\/10.1145\/3062341.3062384","DOI":"10.1145\/3062341.3062384"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A.: 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","DOI":"10.1007\/978-3-319-08867-9_10"},{"key":"3_CR5","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.-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","DOI":"10.1007\/978-3-030-31784-3_16"},{"key":"3_CR6","doi-asserted-by":"publisher","unstructured":"Backes, J., et\u00a0al.: 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":"3_CR7","doi-asserted-by":"publisher","unstructured":"Barbosa, H.: 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","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"3_CR8","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). www.SMT-LIB.org"},{"key":"3_CR9","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1016\/j.tcs.2022.12.009","volume":"943","author":"M Berzish","year":"2023","unstructured":"Berzish, M., et al.: 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","journal-title":"Theor. Comput. Sci."},{"key":"3_CR10","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":"3_CR11","doi-asserted-by":"publisher","unstructured":"Berzish, M.: An SMT solver for regular expressions and linear arithmetic over string length. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021, Part II. LNCS, vol. 12760, pp. 289\u2013312. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_14","DOI":"10.1007\/978-3-030-81688-9_14"},{"key":"3_CR12","unstructured":"Berzish, Murphy: Z3str4: A Solver for Theories over Strings. Ph.D. thesis (2021). http:\/\/hdl.handle.net\/10012\/17102"},{"key":"3_CR13","doi-asserted-by":"publisher","unstructured":"Blahoudek, F.: Word equations in synergy with regular constraints. In: Chechik, M., Katoen, J.P., Leucker, M. (eds.) Formal Methods, pp. 403\u2013423. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_23","DOI":"10.1007\/978-3-031-27481-7_23"},{"key":"3_CR14","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-025-09379-w","author":"F Blahoudek","year":"2025","unstructured":"Blahoudek, F., et al.: Word equations in synergy with regular constraints (extended version). Constraints (2025). https:\/\/doi.org\/10.1007\/s10601-025-09379-w","journal-title":"Constraints"},{"key":"3_CR15","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","DOI":"10.1145\/3158091"},{"key":"3_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3498707","volume":"6","author":"T Chen","year":"2022","unstructured":"Chen, T.: Solving string constraints with regex-dependent functions through transducers with priorities and variables. Proc. ACM Program. Lang 6, 1\u201331 (2022). https:\/\/doi.org\/10.1145\/3498707 POPL","journal-title":"Proc. ACM Program. Lang"},{"key":"3_CR17","doi-asserted-by":"publisher","unstructured":"Chen, T.: 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","DOI":"10.1007\/978-3-030-59152-6_18"},{"key":"3_CR18","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","DOI":"10.1145\/3290362"},{"key":"3_CR19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57246-3_2","author":"YF Chen","year":"2024","unstructured":"Chen, Y.F., Chocholat\u00fd, D., Havlena, V., Hol\u00edk, L., Leng\u00e1l, O., S\u00ed\u010d, J.: Tools and Algorithms for the Construction and Analysis of Systems. Presented at the (2024). https:\/\/doi.org\/10.1007\/978-3-031-57246-3_2 Z3-Noodler: an automata-based string solver","journal-title":"Presented at the"},{"key":"3_CR20","unstructured":"Chen, Y.F., et\u00a0al.: Z3-noodler: an automata-based SMT string solver (2026). https:\/\/github.com\/VeriFIT\/z3-noodler"},{"key":"3_CR21","doi-asserted-by":"crossref","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), (2023). https:\/\/doi.org\/10.1145\/3622872","DOI":"10.1145\/3622872"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Chocholat\u00fd, D., Havlena, V., Hol\u00edk, L., Hrani\u010dka, J., Leng\u00e1l, O., S\u00ed\u010d, J.: Z3-Noodler 1.3: shepherding decision procedures for strings with model generation. In: Tools and Algorithms for the Construction and Analysis of Systems, Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-90653-42","DOI":"10.1007\/978-3-031-90653-4_2"},{"key":"3_CR23","doi-asserted-by":"publisher","unstructured":"Chocholat\u00fd, D., Havlena, V., Hol\u00edk, L., S\u00ed\u010d, J., \u0160ed\u00fd, M.: Artifact for the CAV\u201926 paper \u201cstring solving with stabilization and transducers\u201d (2026)https:\/\/doi.org\/10.5281\/zenodo.19814331","DOI":"10.5281\/zenodo.19814331"},{"key":"3_CR24","doi-asserted-by":"publisher","unstructured":"Chocholat\u00fd, D., Havlena, V., Hol\u00edk, L., S\u00ed\u010d, J., \u0160ed\u00fd, M.: String solving with stabilization and transducers (technical report) (2026). https:\/\/doi.org\/10.48550\/arXiv.2605.14872","DOI":"10.48550\/arXiv.2605.14872"},{"key":"3_CR25","doi-asserted-by":"publisher","unstructured":"Day, J.D., Ehlers, T., Kulczynski, M., Manea, F., Nowotka, D., Poulsen, D.B.: In: Filiot, E., Jungers, R., Potapov, I. (eds.) On solving word equations using SAT. LNCS, vol. 11674, pp. 93\u2013106. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30806-3_8 RP 2019","DOI":"10.1007\/978-3-030-30806-3_8"},{"key":"3_CR26","doi-asserted-by":"publisher","unstructured":"Day, J.D., Ganesh, V., Grewal, N., Manea, F.: On the expressive power of string constraints. Proc. ACM Program. Lang. 7(POPL), 278\u2013308 (2023)https:\/\/doi.org\/10.1145\/3571203","DOI":"10.1145\/3571203"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Eisenhofer, C., Seiser, T., Bj\u00f8rner, N., Kov\u00e1cs, L.: Automated Reasoning with Analytic Tableaux and Related Methods. In: On solving string equations via powers and parikh images, (2026). https:\/\/doi.org\/10.1007\/978-3-032-06085-3_7 Presented at the","DOI":"10.1007\/978-3-032-06085-3_7"},{"key":"3_CR28","unstructured":"Fu, X., Li, C.: Modeling regular replacement for string constraint solving. In: Mu\u00f1oz, C.A. (ed.) Second NASA Formal Methods Symposium - NFM 2010, Washington D.C., USA, April 13-15, 2010. Proceedings. NASA Conference Proceedings, vol. NASA\/CP-2010-216215, pp. 67\u201376 (2010)"},{"key":"3_CR29","doi-asserted-by":"publisher","unstructured":"Hague, M., Hu, D., Je\u017c, A., Lin, A.W., Markgraf, O., R\u00fcmmer, P., Wu, Z.: OSTRICH2: Solver for complex string constraints. In: Irfan, A., Kaufmann, D. (eds.) Proceedings of the 25th Conference on Formal Methods in Computer-Aided Design \u2013 FMCAD 2025, pp. 145\u2013158. TU Wien Academic Press (2025)https:\/\/doi.org\/10.34727\/2025\/isbn.978-3-85448-084-6_21","DOI":"10.34727\/2025\/isbn.978-3-85448-084-6_21"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Hague, M., Je\u017c, A., Lin, A.W., Markgraf, O., R\u00fcmmer, P.: The power of regular constraint propagation. Proc. ACM Program. Lang 9(OOPSLA2), (2025). https:\/\/doi.org\/10.1145\/3763165","DOI":"10.1145\/3763165"},{"key":"3_CR31","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":"3_CR32","doi-asserted-by":"publisher","unstructured":"Hol\u00edk, L., Jank\u016f, 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). https:\/\/doi.org\/10.1145\/3158092","DOI":"10.1145\/3158092"},{"key":"3_CR33","doi-asserted-by":"publisher","unstructured":"Jiang, H., Lin, A.W., Markgraf, O., R\u00fcmmer, P., Stan, D.: HornStr: invariant synthesis for regular model checking as constrained horn clauses. In: Piskac, R., Rakamari\u0107, Z. (eds.) Computer Aided Verification, pp. 200\u2013214. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-98668-0_10","DOI":"10.1007\/978-3-031-98668-0_10"},{"key":"3_CR34","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","DOI":"10.1145\/2837614.2837641"},{"key":"3_CR35","doi-asserted-by":"publisher","unstructured":"Lorentz, R.J.: Creating difficult instances of the post correspondence problem. In: Marsland, T., Frank, I. (eds.) CG 2000. LNCS, vol. 2063, pp. 214\u2013228. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45579-5_14","DOI":"10.1007\/3-540-45579-5_14"},{"key":"3_CR36","doi-asserted-by":"publisher","unstructured":"Lotz, K.: Solving string constraints using SAT. In: Enea, C., Lal, A. (eds.) CAV\u201923. LNCS, vol. 13965, pp. 187\u2013208. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_9","DOI":"10.1007\/978-3-031-37703-7_9"},{"key":"3_CR37","doi-asserted-by":"publisher","unstructured":"Lotz, K., Kulczynski, M., Nowotka, D.: s2s: an eager SMT solver for strings. In: Irfan, A., Kaufmann, D. (eds.) Proceedings of the 25th Conference on Formal Methods in Computer-Aided Design \u2013 FMCAD 2025. pp. 133\u2013138. TU Wien Academic Press (2025)https:\/\/doi.org\/10.34727\/2025\/isbn.978-3-85448-084-6_19","DOI":"10.34727\/2025\/isbn.978-3-85448-084-6_19"},{"key":"3_CR38","unstructured":"Markgraf, O.: 4 different benchmark sets focused around str.replace_all (2025). https:\/\/github.com\/SMT-LIB\/benchmark-submission\/pull\/7, GitHub pull request"},{"key":"3_CR39","doi-asserted-by":"publisher","unstructured":"Morvan, C.: On rational graphs. In: Tiuryn, J. (ed.) FoSSaCS 2000. LNCS, vol. 1784, pp. 252\u2013266. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46432-8_17","DOI":"10.1007\/3-540-46432-8_17"},{"key":"3_CR40","doi-asserted-by":"publisher","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","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"3_CR41","unstructured":"Myreen, M., Leng\u00e1l, O.: Cav 2026 artifact evaluation vm - ubuntu 24.04.4 lts, (2026). https:\/\/doi.org\/10.5281\/zenodo.19184839"},{"key":"3_CR42","doi-asserted-by":"publisher","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., Springe, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_11","DOI":"10.1007\/978-3-031-13188-2_11"},{"key":"3_CR43","doi-asserted-by":"publisher","unstructured":"Omori, A., Minamide, Y.: Further tackling post correspondence problem and proof generation. In: Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP \u201925, pp. 231\u2013242. Association for Computing Machinery, New York, NY, USA (2025). https:\/\/doi.org\/10.1145\/3703595.3705886","DOI":"10.1145\/3703595.3705886"},{"key":"3_CR44","unstructured":"Preiner, M., Schurr, H.J., Barrett, C., Fontaine, P., Niemetz, A., Tinelli, C.: SMT-LIB release 2025 (non-incremental benchmarks, (2025). https:\/\/doi.org\/10.5281\/zenodo.16740866"},{"key":"3_CR45","doi-asserted-by":"publisher","unstructured":"Rungta, N.: A billion SMT queries a day. In: Shoham, S., Vizel, Y. (eds.) CAV 2022, Part I. LNCS, vol. 13371, pp. 3\u201318. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_1 invited paper","DOI":"10.1007\/978-3-031-13185-1_1"},{"key":"3_CR46","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. PLDI 2021, pp. 620\u2013635. Association for Computing Machinery, New York, NY, USA (2021). https:\/\/doi.org\/10.1145\/3453483.3454066","DOI":"10.1145\/3453483.3454066"},{"key":"3_CR47","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1145\/2660267.2660372","DOI":"10.1145\/2660267.2660372"},{"key":"3_CR48","doi-asserted-by":"publisher","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","DOI":"10.1007\/978-3-319-41528-4_12"},{"key":"3_CR49","doi-asserted-by":"publisher","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","DOI":"10.1007\/978-3-642-12002-2_13"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32526-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:45:31Z","timestamp":1784796331000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32526-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325259","9783032325266"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32526-6_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}