{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,23]],"date-time":"2025-09-23T02:07:46Z","timestamp":1758593266427,"version":"3.44.0"},"reference-count":51,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2025,8,4]],"date-time":"2025-08-04T00:00:00Z","timestamp":1754265600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,8,4]],"date-time":"2025-08-04T00:00:00Z","timestamp":1754265600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100003385","name":"Georg-August-Universit\u00e4t G\u00f6ttingen","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100003385","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2025,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Modern SMT solvers, such as Z3, allow solver users to customize strategies to improve performance on their specific use cases. However, handcrafting an optimized strategy for a specific class of SMT instances remains a complex and demanding task for both solver developers and users alike. In this paper, we address the problem of automated SMT strategy synthesis via a novel method based on Monte-Carlo Tree Search (MCTS). We formulate strategy synthesis as a sequential decision-making process, where the search tree corresponds to the strategy space. Subsequently, we employ MCTS to navigate this vast search space. Compared to the conventional MCTS, we introduce two heuristics\u2014layered and staged search\u2014that enable our method to identify effective strategies with lower costs. We implement our method, dubbed Z3alpha, upon the Z3 SMT solver. Our experiments demonstrate that Z3alpha outperforms the default Z3 solver and the state-of-the-art synthesis tool Fastsmt on the majority of the evaluated benchmark sets, while producing more interpretable strategies than FastSMT. At SMT-COMP\u201924, among the 16 participating logics, Z3alpha improved upon the default Z3 in 12 cases and helped solve hundreds more instances in QF_NIA and QF_NRA, winning their respective divisions.<\/jats:p>","DOI":"10.1007\/s00236-025-00495-x","type":"journal-article","created":{"date-parts":[[2025,8,4]],"date-time":"2025-08-04T19:48:33Z","timestamp":1754336913000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Novel tree-search method for synthesizing SMT strategies"],"prefix":"10.1007","volume":"62","author":[{"given":"Zhengyang John","family":"Lu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joel","family":"Day","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Piyush","family":"Jha","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paul","family":"Sarnighausen-Cahn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Siemer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florin","family":"Manea","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vijay","family":"Ganesh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,8,4]]},"reference":[{"issue":"9","key":"495_CR1","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"L De Moura","year":"2011","unstructured":"De Moura, L., Bj\u00f8rner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69\u201377 (2011)","journal-title":"Commun. ACM"},{"issue":"2","key":"495_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1455518.1455522","volume":"12","author":"C Cadar","year":"2008","unstructured":"Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: Automatically generating inputs of death. ACM Transactions on Information and System Security (TISSEC) 12(2), 1\u201338 (2008)","journal-title":"ACM Transactions on Information and System Security (TISSEC)"},{"key":"495_CR3","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: International Conference on Computer Aided Verification, pp. 343\u2013361 (2015). Springer","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"495_CR4","doi-asserted-by":"crossref","unstructured":"Song, D., Brumley, D., Yin, H., Caballero, J., Jager, I., Kang, M.G., Liang, Z., Newsome, J., Poosankam, P., Saxena, P.: BitBlaze: A new approach to computer security via binary analysis. In: Information Systems Security: 4th International Conference, ICISS 2008, Hyderabad, India, December 16-20, 2008. Proceedings 4, pp. 1\u201325 (2008). Springer","DOI":"10.1007\/978-3-540-89862-7_1"},{"issue":"2","key":"495_CR5","doi-asserted-by":"publisher","first-page":"117","DOI":"10.3233\/AIC-2012-0525","volume":"25","author":"L Pulina","year":"2012","unstructured":"Pulina, L., Tacchella, A.: Challenging SMT solvers to verify neural networks. AI Commun. 25(2), 117\u2013135 (2012)","journal-title":"AI Commun."},{"key":"495_CR6","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340 (2008). Springer","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"495_CR7","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Passmore, G.O.: The strategy challenge in SMT solving. Automated Reasoning and Mathematics: Essays in Memory of William W. McCune, 15\u201344 (2013)","DOI":"10.1007\/978-3-642-36675-8_2"},{"key":"495_CR8","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). http:\/\/smtlib.cs.uiowa.edu\/index.shtml. Accessed: 2024-01-16 (2016)"},{"key":"495_CR9","doi-asserted-by":"crossref","unstructured":"Ram\u00edrez, N.G., Hamadi, Y., Monfroy, E., Saubion, F.: Evolving SMT strategies. In: 2016 IEEE 28th International Conference on Tools with Artificial Intelligence (ICTAI), pp. 247\u2013254 (2016). IEEE","DOI":"10.1109\/ICTAI.2016.0046"},{"key":"495_CR10","unstructured":"Balunovic, M., Bielik, P., Vechev, M.: Learning to solve SMT formulas. In: Advances in Neural Information Processing Systems 31, pp. 10337\u201310348 (2018). http:\/\/papers.nips.cc\/paper\/8233-learning-to-solve-smt-formulas.pdf"},{"key":"495_CR11","doi-asserted-by":"publisher","unstructured":"Coulom, R.: Efficient selectivity and backup operators in Monte-Carlo tree search. In: Herik, H.J., Ciancarini, P., Donkers, H.H.L.M. (eds.) Computers and Games, 5th International Conference, CG 2006, Turin, Italy, May 29-31, 2006. Revised Papers. Lecture Notes in Computer Science, vol. 4630, pp. 72\u201383. Springer,??? (2006). https:\/\/doi.org\/10.1007\/978-3-540-75538-8_7","DOI":"10.1007\/978-3-540-75538-8_7"},{"key":"495_CR12","doi-asserted-by":"publisher","unstructured":"Kocsis, L., Szepesv\u00e1ri, C.: Bandit based Monte-Carlo planning. In: F\u00fcrnkranz, J., Scheffer, T., Spiliopoulou, M. (eds.) Machine Learning: ECML 2006, 17th European Conference on Machine Learning, Berlin, Germany, September 18-22, 2006, Proceedings. Lecture Notes in Computer Science, vol. 4212, pp. 282\u2013293 (2006). https:\/\/doi.org\/10.1007\/11871842_29","DOI":"10.1007\/11871842_29"},{"issue":"7587","key":"495_CR13","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1038\/nature16961","volume":"529","author":"D Silver","year":"2016","unstructured":"Silver, D., Huang, A., Maddison, C.J., Guez, A., Sifre, L., Van Den Driessche, G., Schrittwieser, J., Antonoglou, I., Panneershelvam, V., Lanctot, M., et al.: Mastering the game of Go with deep neural networks and tree search. nature 529(7587), 484\u2013489 (2016)","journal-title":"nature"},{"key":"495_CR14","unstructured":"Silver, D., Hubert, T., Schrittwieser, J., Antonoglou, I., Lai, M., Guez, A., Lanctot, M., Sifre, L., Kumaran, D., Graepel, T., et al.: Mastering chess and shogi by self-play with a general reinforcement learning algorithm. arXiv preprint arXiv:1712.01815 (2017)"},{"issue":"11","key":"495_CR15","doi-asserted-by":"publisher","first-page":"2894","DOI":"10.1109\/TCAD.2018.2858463","volume":"37","author":"Z Zhang","year":"2018","unstructured":"Zhang, Z., Ernst, G., Sedwards, S., Arcaini, P., Hasuo, I.: Two-layered falsification of hybrid systems guided by Monte Carlo tree search. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 37(11), 2894\u20132905 (2018)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"495_CR16","doi-asserted-by":"crossref","unstructured":"Khalil, E.B., Vaezipoor, P., Dilkina, B.: Finding backdoors to integer programs: a Monte Carlo tree search framework. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 36, pp. 3786\u20133795 (2022)","DOI":"10.1609\/aaai.v36i4.20293"},{"key":"495_CR17","unstructured":"Sun, F., Liu, Y., Wang, J., Sun, H.: Symbolic physics learner: Discovering governing equations via Monte Carlo tree search. In: The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1\u20135, 2023 (2023). https:\/\/openreview.net\/forum?id=ZTK3SefE8_Z"},{"key":"495_CR18","doi-asserted-by":"publisher","unstructured":"Lu, Z., Siemer, S., Jha, P., Day, J., Manea, F., Ganesh, V.: Layered and staged monte carlo tree search for smt strategy synthesis. In: Larson, K. (ed.) Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI-24, pp. 1907\u20131915. International Joint Conferences on Artificial Intelligence Organization, Jeju Island, South Korea (2024). https:\/\/doi.org\/10.24963\/ijcai.2024\/211. Main Track","DOI":"10.24963\/ijcai.2024\/211"},{"issue":"1","key":"495_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/TCIAIG.2012.2186810","volume":"4","author":"CB Browne","year":"2012","unstructured":"Browne, C.B., Powley, E., Whitehouse, D., Lucas, S.M., Cowling, P.I., Rohlfshagen, P., Tavener, S., Perez, D., Samothrakis, S., Colton, S.: A survey of Monte Carlo tree search methods. IEEE Transactions on Computational Intelligence and AI in games 4(1), 1\u201343 (2012)","journal-title":"IEEE Transactions on Computational Intelligence and AI in games"},{"key":"495_CR20","doi-asserted-by":"publisher","unstructured":"Cameron, C., Hartford, J.S., Lundy, T., Truong, T., Milligan, A., Chen, R., Leyton-Brown, K.: UNSAT solver synthesis via Monte Carlo Forest Search. In: Dilkina, B. (ed.) Integration of Constraint Programming, Artificial Intelligence, and Operations Research - 21st International Conference, CPAIOR 2024, Uppsala, Sweden, May 28-31, 2024, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14742, pp. 170\u2013189 (2024). https:\/\/doi.org\/10.1007\/978-3-031-60597-0_12","DOI":"10.1007\/978-3-031-60597-0_12"},{"key":"495_CR21","unstructured":"Jha, P., Li, Z., Lu, Z., Bright, C., Ganesh, V.: AlphaMapleSAT: An MCTS-based cube-and-conquer SAT solver for hard combinatorial problems. arXiv preprint arXiv:2401.13770 (2024)"},{"issue":"7964","key":"495_CR22","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1038\/s41586-023-06004-9","volume":"618","author":"DJ Mankowitz","year":"2023","unstructured":"Mankowitz, D.J., Michi, A., Zhernov, A., Gelmi, M., Selvi, M., Paduraru, C., Leurent, E., Iqbal, S., Lespiau, J.-B., Ahern, A., et al.: Faster sorting algorithms discovered using deep reinforcement learning. Nature 618(7964), 257\u2013263 (2023)","journal-title":"Nature"},{"key":"495_CR23","doi-asserted-by":"publisher","unstructured":"Parsert, J., Polgreen, E.: Reinforcement learning and data-generation for syntax-guided synthesis. In: Wooldridge, M.J., Dy, J.G., Natarajan, S. (eds.) Thirty-Eighth AAAI Conference on Artificial Intelligence, AAAI 2024, Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence, IAAI 2024, Fourteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2014, February 20-27, 2024, Vancouver, Canada, pp. 10670\u201310678 (2024). https:\/\/doi.org\/10.1609\/AAAI.V38I9.28938","DOI":"10.1609\/AAAI.V38I9.28938"},{"issue":"11","key":"495_CR24","doi-asserted-by":"publisher","first-page":"1856","DOI":"10.1016\/j.artint.2011.03.007","volume":"175","author":"S Gelly","year":"2011","unstructured":"Gelly, S., Silver, D.: Monte-Carlo tree search and rapid action value estimation in computer Go. Artif. Intell. 175(11), 1856\u20131875 (2011)","journal-title":"Artif. Intell."},{"key":"495_CR25","unstructured":"Johanson, M.: Measuring the size of large no-limit poker games. arXiv preprint arXiv:1302.7008 (2013)"},{"key":"495_CR26","doi-asserted-by":"crossref","unstructured":"De\u00a0Waard, M., Roijers, D.M., Bakkes, S.C.: Monte Carlo tree search with options for general video game playing. In: 2016 IEEE Conference on Computational Intelligence and Games (CIG), pp. 1\u20138 (2016). IEEE","DOI":"10.1109\/CIG.2016.7860383"},{"issue":"1\u20132","key":"495_CR27","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/S0004-3702(99)00052-1","volume":"112","author":"RS Sutton","year":"1999","unstructured":"Sutton, R.S., Precup, D., Singh, S.: Between MDPs and semi-MDPs: A framework for temporal abstraction in reinforcement learning. Artif. Intell. 112(1\u20132), 181\u2013211 (1999)","journal-title":"Artif. Intell."},{"key":"495_CR28","doi-asserted-by":"publisher","unstructured":"Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: Satzilla: Portfolio-based algorithm selection for SAT. J. Artif. Intell. Res. 32, 565\u2013606 (2008) https:\/\/doi.org\/10.1613\/jair.2490","DOI":"10.1613\/jair.2490"},{"key":"495_CR29","doi-asserted-by":"publisher","unstructured":"Scott, J., Niemetz, A., Preiner, M., Nejati, S., Ganesh, V.: Machsmt: A machine learning-based algorithm selector for SMT solvers. In: Groote, J.F., Larsen, K.G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12652, pp. 303\u2013325 (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_16","DOI":"10.1007\/978-3-030-72013-1_16"},{"key":"495_CR30","doi-asserted-by":"crossref","unstructured":"Lu, Z., Chien, P.-C., Lee, N.-Z., Gurfinkel, A., Ganesh, V.: Btor2-Select: Machine learning based algorithm selection for hardware model checking. In: Proc. CAV (2025). Springer","DOI":"10.1007\/978-3-031-98668-0_15"},{"key":"495_CR31","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1613\/jair.2861","volume":"36","author":"F Hutter","year":"2009","unstructured":"Hutter, F., Hoos, H.H., Leyton-Brown, K., St\u00fctzle, T.: ParamILS: an automatic algorithm configuration framework. Journal of artificial intelligence research 36, 267\u2013306 (2009)","journal-title":"Journal of artificial intelligence research"},{"key":"495_CR32","doi-asserted-by":"crossref","unstructured":"Hutter, F., Hoos, H.H., Leyton-Brown, K.: Sequential model-based optimization for general algorithm configuration. In: Learning and Intelligent Optimization: 5th International Conference, LION 5, Rome, Italy, January 17-21, 2011. Selected Papers 5, pp. 507\u2013523 (2011). Springer","DOI":"10.1007\/978-3-642-25566-3_40"},{"key":"495_CR33","doi-asserted-by":"crossref","unstructured":"Kadioglu, S., Malitsky, Y., Sabharwal, A., Samulowitz, H., Sellmann, M.: Algorithm selection and scheduling. In: Principles and Practice of Constraint Programming\u2013CP 2011: 17th International Conference, CP 2011, Perugia, Italy, September 12\u201316, 2011. Proceedings 17, pp. 454\u2013469 (2011). Springer","DOI":"10.1007\/978-3-642-23786-7_35"},{"key":"495_CR34","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1613\/jair.1.13676","volume":"75","author":"E Schede","year":"2022","unstructured":"Schede, E., Brandt, J., Tornede, A., Wever, M., Bengs, V., H\u00fcllermeier, E., Tierney, K.: A survey of methods for automated algorithm configuration. Journal of Artificial Intelligence Research 75, 425\u2013487 (2022)","journal-title":"Journal of Artificial Intelligence Research"},{"issue":"2","key":"495_CR35","doi-asserted-by":"publisher","first-page":"1162","DOI":"10.1111\/ITOR.12650","volume":"27","author":"NG Ram\u00edrez","year":"2020","unstructured":"Ram\u00edrez, N.G., Monfroy, \u00c9., Saubion, F., Castro, C.: Improving complex SMT strategies with learning. Int. Trans. Oper. Res. 27(2), 1162\u20131188 (2020). https:\/\/doi.org\/10.1111\/ITOR.12650","journal-title":"Int. Trans. Oper. Res."},{"key":"495_CR36","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/BF00175355","volume":"4","author":"JR Koza","year":"1994","unstructured":"Koza, J.R.: Genetic programming as a means for programming computers by natural selection. Stat. Comput. 4, 87\u2013112 (1994)","journal-title":"Stat. Comput."},{"key":"495_CR37","unstructured":"Ross, S., Gordon, G., Bagnell, D.: A reduction of imitation learning and structured prediction to no-regret online learning. In: Proceedings of the Fourteenth International Conference on Artificial Intelligence and Statistics, pp. 627\u2013635 (2011). JMLR Workshop and Conference Proceedings"},{"key":"495_CR38","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511794797","volume-title":"Artificial Intelligence: Foundations of Computational Agents","author":"DL Poole","year":"2010","unstructured":"Poole, D.L., Mackworth, A.K.: Artificial Intelligence: Foundations of Computational Agents. Cambridge University Press, Cambridge, UK (2010)"},{"key":"495_CR39","doi-asserted-by":"crossref","unstructured":"Chen, Z., Chen, Z., Shuai, Z., Zhang, G., Pan, W., Zhang, Y., Wang, J.: Synthesize solving strategy for symbolic execution. In: Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 348\u2013360 (2021)","DOI":"10.1145\/3460319.3464815"},{"key":"495_CR40","unstructured":"Lu, Z.: AlphaSMT: A reinforcement learning guided SMT solver. Master\u2019s thesis, University of Waterloo (2023)"},{"key":"495_CR41","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-50497-0","volume-title":"Decision Procedures: An Alogorithm Point of View","author":"D Kroening","year":"2016","unstructured":"Kroening, D., Strichman, O.: Decision Procedures: An Alogorithm Point of View. Springer, Cham, Switzerland (2016)"},{"key":"495_CR42","unstructured":"Bobot, F., Bromberger, M., Hoenicke, J.: SMT-COMP 2023. https:\/\/smt-comp.github.io\/2023\/. Accessed: 2024-01-16 (2023)"},{"key":"495_CR43","unstructured":"Microsoft: Online Z3 Guide. https:\/\/microsoft.github.io\/z3guide\/. Accessed: 2024-01-16 (2023)"},{"key":"495_CR44","doi-asserted-by":"crossref","unstructured":"Kocsis, L., Szepesv\u00e1ri, C.: Bandit based monte-carlo planning. In: European Conference on Machine Learning, pp. 282\u2013293 (2006). Springer","DOI":"10.1007\/11871842_29"},{"key":"495_CR45","doi-asserted-by":"crossref","unstructured":"Sabharwal, A., Samulowitz, H., Reddy, C.: Guiding combinatorial optimization with UCT. In: Integration of AI and OR Techniques in Contraint Programming for Combinatorial Optimzation Problems: 9th International Conference, CPAIOR 2012, Nantes, France, May 28\u2013June1, 2012. Proceedings 9, pp. 356\u2013361 (2012). Springer","DOI":"10.1007\/978-3-642-29828-8_23"},{"issue":"5","key":"495_CR46","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1090\/S0002-9904-1952-09620-8","volume":"58","author":"H Robbins","year":"1952","unstructured":"Robbins, H.: Some aspects of the sequential design of experiments. Bull. Amer. Math. Soc. 58(5), 527\u2013535 (1952)","journal-title":"Bull. Amer. Math. Soc."},{"key":"495_CR47","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). IEEE","DOI":"10.23919\/FMCAD.2017.8102241"},{"key":"495_CR48","doi-asserted-by":"crossref","unstructured":"Mora, F., Berzish, M., Kulczynski, M., Nowotka, D., Ganesh, V.: Z3str4: A multi-armed string solver. In: Formal Methods: 24th International Symposium, FM 2021, Virtual Event, November 20\u201326, 2021, Proceedings 24, pp. 389\u2013406 (2021). Springer","DOI":"10.1007\/978-3-030-90870-6_21"},{"key":"495_CR49","doi-asserted-by":"crossref","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: International Conference on Computer Aided Verification, pp. 289\u2013312 (2021). Springer","DOI":"10.1007\/978-3-030-81688-9_14"},{"key":"495_CR50","unstructured":"Bromberger, M., Bobot, F., Jon\u00e1\u0161, M.: The 19th International Satisfiability Modulo Theories Competition (SMT-COMP 2024). https:\/\/smt-comp.github.io\/2024\/. Accessed: 2024-10-17 (2024)"},{"key":"495_CR51","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Reliable and reproducible competition results with benchexec and witnesses (report on SV-COMP 2016). In: Chechik, M., Raskin, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9636, pp. 887\u2013904 (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_55","DOI":"10.1007\/978-3-662-49674-9_55"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-025-00495-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-025-00495-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-025-00495-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,22]],"date-time":"2025-09-22T06:26:13Z","timestamp":1758522373000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-025-00495-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,4]]},"references-count":51,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9]]}},"alternative-id":["495"],"URL":"https:\/\/doi.org\/10.1007\/s00236-025-00495-x","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2025,8,4]]},"assertion":[{"value":"15 December 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 June 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 August 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"28"}}