{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:21:18Z","timestamp":1779074478170,"version":"3.51.4"},"publisher-location":"Cham","reference-count":56,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986673","type":"print"},{"value":"9783031986680","type":"electronic"}],"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,7,22]],"date-time":"2025-07-22T00:00:00Z","timestamp":1753142400000},"content-version":"vor","delay-in-days":202,"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                    In recent years, a diverse variety of hardware model-checking tools and techniques that exhibit complementary strengths and distinct weaknesses have been proposed. This state of affairs naturally suggests the use of algorithm-selection techniques to select the right tool for a given instance. To automate this process, we present\n                    <jats:sc>Btor2-Select<\/jats:sc>\n                    , a machine learning-based algorithm-selection framework for the hardware model-checking problem described in the word-level modeling language\n                    <jats:sc>Btor2<\/jats:sc>\n                    . The framework offers an efficient and effective machine-learning pipeline for training an algorithm selector.\n                    <jats:sc>Btor2-Select<\/jats:sc>\n                    also enables the use of the trained selector to predict the most suitable off-the-shelf model checker for a given verification task and automatically invoke it to solve the task. Evaluated on a comprehensive\n                    <jats:sc>Btor2<\/jats:sc>\n                    benchmark suite coupled with a set of state-of-the-art model checkers,\n                    <jats:sc>Btor2-Select<\/jats:sc>\n                    trained an algorithm selector that successfully closed over 65\u00a0% of the PAR-2 performance gap between the best single tool and the idealized virtual selector. Moreover, the selector outperformed a portfolio model checker that runs three complementary verification engines in parallel.\n                    <jats:sc>Btor2-Select<\/jats:sc>\n                    offers a simple, systematic, and extensible solution to harness the complementary strengths of diverse model checkers. With its fast and highly configurable training procedure,\n                    <jats:sc>Btor2-Select<\/jats:sc>\n                    can be easily integrated with new tools and applied to various application domains.\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-98668-0_15","type":"book-chapter","created":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T20:46:03Z","timestamp":1753130763000},"page":"296-311","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Btor2-Select:\u00a0Machine\u00a0Learning\u00a0Based\u00a0Algorithm Selection for Hardware Model Checking"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-9046-497X","authenticated-orcid":false,"given":"Zhengyang","family":"Lu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5139-5178","authenticated-orcid":false,"given":"Po-Chun","family":"Chien","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8096-5595","authenticated-orcid":false,"given":"Nian-Ze","family":"Lee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5964-6792","authenticated-orcid":false,"given":"Arie","family":"Gurfinkel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6029-2047","authenticated-orcid":false,"given":"Vijay","family":"Ganesh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,7,22]]},"reference":[{"key":"15_CR1","unstructured":"Hardware model-checking competition (HWMCC). https:\/\/hwmcc.github.io\/. Accessed 14 Jan 2025"},{"key":"15_CR2","doi-asserted-by":"publisher","unstructured":"Balcan, M.F., Sandholm, T., Vitercik, E.: Generalization in portfolio-based algorithm selection. In: Proc. AAAI, vol.\u00a035, pp. 12225\u201312232. AAAI Press (2021). https:\/\/doi.org\/10.1609\/aaai.v35i14.17451","DOI":"10.1609\/aaai.v35i14.17451"},{"key":"15_CR3","doi-asserted-by":"publisher","unstructured":"Beyer, D., Chien, P.C., Jankola, M.: BenchCloud: A platform for scalable performance benchmarking. In: Proc. ASE, pp. 2386\u20132389. ACM (2024). https:\/\/doi.org\/10.1145\/3691620.3695358","DOI":"10.1145\/3691620.3695358"},{"key":"15_CR4","doi-asserted-by":"publisher","unstructured":"Beyer, D., Chien, P.C., Lee, N.Z.: Bridging hardware and software analysis with Btor2C: A word-level-circuit-to-C translator. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023. LNCS, vol. 13994, pp. 152\u2013172. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_12","DOI":"10.1007\/978-3-031-30820-8_12"},{"issue":"1","key":"15_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10009-017-0469-y","volume":"21","author":"D Beyer","year":"2017","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: Requirements and solutions. Int. J. Softw. Tools Technol. Transfer 21(1), 1\u201329 (2017). https:\/\/doi.org\/10.1007\/s10009-017-0469-y","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"15_CR6","doi-asserted-by":"publisher","unstructured":"Biere, A., Froleyks, N., Preiner, M.: Hardware model checking competition 2024. In: Proc. FMCAD, p.\u00a07. TU Wien Academic Press (2024). https:\/\/doi.org\/10.34727\/2024\/isbn.978-3-85448-065-5_6","DOI":"10.34727\/2024\/isbn.978-3-85448-065-5_6"},{"key":"15_CR7","doi-asserted-by":"publisher","unstructured":"Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Technical report,\u00a011\/2, Institute for Formal Models and Verification, Johannes Kepler University (2011). https:\/\/doi.org\/10.35011\/fmvtr.2011-2","DOI":"10.35011\/fmvtr.2011-2"},{"key":"15_CR8","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117\u2013148 (2003). https:\/\/doi.org\/10.1016\/S0065-2458(03)58003-2","journal-title":"Adv. Comput."},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"Computer Aided Verification","author":"R Brayton","year":"2010","unstructured":"Brayton, R., Mishchenko, A.: ABC: An academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24\u201340. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_5"},{"key":"15_CR11","unstructured":"Brayton, R.K., E\u00e9n, N., Mishchenko, A.: Using speculation for sequential equivalence checking. In: Proc. IWLS (2012)"},{"issue":"1","key":"15_CR12","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/A:1010933404324","volume":"45","author":"L Breiman","year":"2001","unstructured":"Breiman, L.: Random forests. Mach. Learn. 45(1), 5\u201332 (2001). https:\/\/doi.org\/10.1023\/A:1010933404324","journal-title":"Mach. Learn."},{"issue":"2","key":"15_CR13","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/S10703-011-0123-3","volume":"39","author":"G Cabodi","year":"2011","unstructured":"Cabodi, G., Nocco, S., Quer, S.: Benchmarking a model checker for algorithmic improvements and tuning for performance. Formal Methods Syst. Des. 39(2), 205\u2013227 (2011). https:\/\/doi.org\/10.1007\/S10703-011-0123-3","journal-title":"Formal Methods Syst. Des."},{"key":"15_CR14","doi-asserted-by":"publisher","unstructured":"Chen, T., Guestrin, C.: XGBoost: A scalable tree boosting system. In: Proc. KDD, pp. 785\u2013794. ACM (2016). https:\/\/doi.org\/10.1145\/2939672.2939785","DOI":"10.1145\/2939672.2939785"},{"key":"15_CR15","doi-asserted-by":"publisher","unstructured":"Chien, P.C., Lee, N.Z., Lu, Z.: Performance dataset for hardware model checking on Btor2 benchmarks (technical report, May 2025). Zenodo (2025). https:\/\/doi.org\/10.5281\/zenodo.15605218","DOI":"10.5281\/zenodo.15605218"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-642-54862-8_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2014","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 46\u201361. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_4"},{"key":"15_CR17","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT (1999). https:\/\/mitpress.mit.edu\/books\/model-checking"},{"key":"15_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15"},{"issue":"3","key":"15_CR19","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/BF00994018","volume":"20","author":"C Cortes","year":"1995","unstructured":"Cortes, C., Vapnik, V.: Support-vector networks. Mach. Learn. 20(3), 273\u2013297 (1995). https:\/\/doi.org\/10.1007\/BF00994018","journal-title":"Mach. Learn."},{"key":"15_CR20","doi-asserted-by":"publisher","unstructured":"Demyanova, Y., Pani, T., Veith, H., Zuleger, F.: Empirical software metrics for benchmarking of verification tools. Formal Methods Syst. Des. 50(2-3), 289\u2013316 (2017). https:\/\/doi.org\/10.1007\/s10703-016-0264-5","DOI":"10.1007\/s10703-016-0264-5"},{"key":"15_CR21","unstructured":"E\u00e9n, N., Mishchenko, A., Brayton, R.K.: Efficient implementation of property directed reachability. In: Proc. FMCAD, pp. 125\u2013134. FMCAD Inc. (2011). https:\/\/dl.acm.org\/doi\/10.5555\/2157654.2157675"},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-030-20652-9_11","volume-title":"NASA Formal Methods","author":"A Goel","year":"2019","unstructured":"Goel, A., Sakallah, K.: Model checking of Verilog RTL using IC3 with syntax-guided abstraction. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2019. LNCS, vol. 11460, pp. 166\u2013185. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-20652-9_11"},{"key":"15_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-030-45190-5_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Goel","year":"2020","unstructured":"Goel, A., Sakallah, K.: AVR: Abstractly verifying reachability. In: TACAS 2020. LNCS, vol. 12078, pp. 413\u2013422. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_23"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-44618-4_10","volume-title":"CONCUR 2000 \u2014 Concurrency Theory","author":"K Heljanko","year":"2000","unstructured":"Heljanko, K.: Model checking with finite complete prefixes is PSPACE-complete. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 108\u2013122. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44618-4_10"},{"key":"15_CR25","doi-asserted-by":"publisher","unstructured":"Jolliffe, I.T.: Principal Component Analysis, 1 edn. Springer, New York (1986). https:\/\/doi.org\/10.1007\/978-1-4757-1904-8","DOI":"10.1007\/978-1-4757-1904-8"},{"key":"15_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"454","DOI":"10.1007\/978-3-642-23786-7_35","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2011","author":"S Kadioglu","year":"2011","unstructured":"Kadioglu, S., Malitsky, Y., Sabharwal, A., Samulowitz, H., Sellmann, M.: Algorithm selection and scheduling. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 454\u2013469. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23786-7_35"},{"key":"15_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/3-540-49519-3_19","volume-title":"Formal Methods in Computer-Aided Design","author":"G Kamhi","year":"1998","unstructured":"Kamhi, G., Fix, L., Binyamini, Z.: Symbolic model checking visualization. In: Gopalakrishnan, G., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 290\u2013302. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-49519-3_19"},{"key":"15_CR28","doi-asserted-by":"publisher","unstructured":"Kerschke, P., Hoos, H.H., Neumann, F., Trautmann, H.: Automated algorithm selection: Survey and perspectives. Evol. Comput. 27(1), 3\u201345 (2019). https:\/\/doi.org\/10.1162\/evco_a_00242","DOI":"10.1162\/evco_a_00242"},{"key":"15_CR29","unstructured":"Kohavi, R.: A study of cross-validation and bootstrap for accuracy estimation and model selection. In: Proc. IJCAI, pp. 1137\u20131145. Morgan Kaufmann (1995). http:\/\/ijcai.org\/Proceedings\/95-2\/Papers\/016.pdf"},{"issue":"7553","key":"15_CR30","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1038\/nature14539","volume":"521","author":"Y LeCun","year":"2015","unstructured":"LeCun, Y., Bengio, Y., Hinton, G.: Deep learning. Nature 521(7553), 436\u2013444 (2015). https:\/\/doi.org\/10.1038\/nature14539","journal-title":"Nature"},{"key":"15_CR31","doi-asserted-by":"publisher","unstructured":"Leeson, W., Dwyer, M.B.: Algorithm selection for software verification using graph neural networks. ACM Trans. Softw. Eng. Methodol. 33(3) (2024). https:\/\/doi.org\/10.1145\/3637225","DOI":"10.1145\/3637225"},{"key":"15_CR32","doi-asserted-by":"publisher","unstructured":"Lu, Z., Chien, P.C., Lee, N.Z., Ganesh, V.: Algorithm selection for word-level hardware model checking (student abstract). In: Proc. AAAI, vol.\u00a039, pp. 29426\u201329427 (2025). https:\/\/doi.org\/10.1609\/aaai.v39i28.35275","DOI":"10.1609\/aaai.v39i28.35275"},{"key":"15_CR33","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.15485472","author":"Z Lu","year":"2025","unstructured":"Lu, Z., Chien, P.C., Lee, N.Z., Gurfinkel, A., Ganesh, V.: Reproduction package for CAV 2025 article \u2018Btor2-Select: machine learning based algorithm selection for hardware model checking\u2019. Zenodo (2025). https:\/\/doi.org\/10.5281\/zenodo.15485472","journal-title":"Zenodo"},{"key":"15_CR34","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.15338910","author":"Z Lu","year":"2025","unstructured":"Lu, Z., Chien, P.C., Lee, N.Z., Gurfinkel, A., Ganesh, V.: Reproduction package for CAV 2025 submission \u2018Btor2-Select: machine learning based algorithm selection for hardware model checking\u2019. Zenodo (2025). https:\/\/doi.org\/10.5281\/zenodo.15338910","journal-title":"Zenodo"},{"key":"15_CR35","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: Proc. IJCAI, pp. 1907\u20131915. IJCAI Org (2024). https:\/\/doi.org\/10.24963\/ijcai.2024\/211","DOI":"10.24963\/ijcai.2024\/211"},{"key":"15_CR36","doi-asserted-by":"publisher","unstructured":"Mann, M., Irfan, A., Lonsing, F., Yang, Y., Zhang, H., Brown, K., Gupta, A., Barrett, C.W.: Pono: a flexible and extensible SMT-based model checker. In: Silva, A., Leino, K. (eds.) CAV 2021. LNCS, vol. 12760, pp. 461\u2013474. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_22","DOI":"10.1007\/978-3-030-81688-9_22"},{"key":"15_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1\u201313. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1"},{"key":"15_CR38","doi-asserted-by":"publisher","unstructured":"Menezes, R., Aldughaim, M., Farias, B., Li, X., Manino, E., Shmarov, F., Song, K., Brau\u00dfe, F., Gadelha, M.R., Tihanyi, N., Korovin, K., Cordeiro, L.: ESBMC v7.4: Harnessing the power of intervals (competition contribution). In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) TACAS 2024. LNCS, vol. 14572, pp. 376\u2013380. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_24","DOI":"10.1007\/978-3-031-57256-2_24"},{"key":"15_CR39","doi-asserted-by":"publisher","unstructured":"Mony, H., Baumgartner, J., Mishchenko, A., Brayton, R.: Speculative reduction-based scalable redundancy identification. In: Proc. DATE, pp. 1674\u20131679. IEEE (2009). https:\/\/doi.org\/10.1109\/DATE.2009.5090932","DOI":"10.1109\/DATE.2009.5090932"},{"key":"15_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/978-3-540-30494-4_12","volume-title":"Formal Methods in Computer-Aided Design","author":"H Mony","year":"2004","unstructured":"Mony, H., Baumgartner, J., Paruthi, V., Kanzelman, R., Kuehlmann, A.: Scalable automated verification via expert-system guided transformations. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 159\u2013173. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30494-4_12"},{"key":"15_CR41","unstructured":"Niemetz, A., Preiner, M., Wolf, C., Biere, A.: Source-code repository of Btor2 tools. https:\/\/github.com\/hwmcc\/btor2tools. Accessed 01 May 2025"},{"key":"15_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"587","DOI":"10.1007\/978-3-319-96145-3_32","volume-title":"Computer Aided Verification","author":"A Niemetz","year":"2018","unstructured":"Niemetz, A., Preiner, M., Wolf, C., Biere, A.: Btor2, BtorMC and Boolector\u00a03.0. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 587\u2013595. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_32"},{"key":"15_CR43","unstructured":"Pedregosa, F., Varoquaux, G., Gramfort, A., Michel, V., Thirion, B., Grisel, O., Blondel, M., Prettenhofer, P., Weiss, R., Dubourg, V., Vanderplas, J., Passos, A., Cournapeau, D., Brucher, M., Perrot, M., Duchesnay, \u00c9.: Scikit-learn: Machine learning in Python. J. Mach. Learn. Res. 12(85), 2825\u20132830 (2011). http:\/\/jmlr.org\/papers\/v12\/pedregosa11a.html"},{"key":"15_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-030-80223-3_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2021","author":"N Pimpalkhare","year":"2021","unstructured":"Pimpalkhare, N., Mora, F., Polgreen, E., Seshia, S.A.: MedleySolver: Online SMT algorithm selection. In: Li, C.-M., Many\u00e0, F. (eds.) SAT 2021. LNCS, vol. 12831, pp. 453\u2013470. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-80223-3_31"},{"key":"15_CR45","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.14156844","author":"M Preiner","year":"2024","unstructured":"Preiner, M., Froleyks, N., Biere, A.: HWMCC \u201924 benchmarks and results. Zenodo (2024). https:\/\/doi.org\/10.5281\/zenodo.14156844","journal-title":"Zenodo"},{"key":"15_CR46","doi-asserted-by":"publisher","unstructured":"Richter, C., H\u00fcllermeier, E., Jakobs, M.C., Wehrheim, H.: Algorithm selection for software validation based on graph kernels. Autom. Softw. Eng. 27(1), 153\u2013186 (2020). https:\/\/doi.org\/10.1007\/s10515-020-00270-x","DOI":"10.1007\/s10515-020-00270-x"},{"key":"15_CR47","doi-asserted-by":"publisher","unstructured":"Richter, C., Wehrheim, H.: Attend and represent: A novel view on algorithm selection for software verification. In: Proc. ASE, pp. 1016\u20131028 (2020). https:\/\/doi.org\/10.1145\/3324884.3416633","DOI":"10.1145\/3324884.3416633"},{"issue":"1","key":"15_CR48","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/S10009-011-0204-Z","volume":"14","author":"GP Safe","year":"2012","unstructured":"Safe, G.P., Coelho, C., Vieira, L., Val, C., Nacif, J., Fernandes, A.O.: Selection of formal verification heuristics for parallel execution. Int. J. Softw. Tools Technol. Transf. 14(1), 95\u2013108 (2012). https:\/\/doi.org\/10.1007\/S10009-011-0204-Z","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"2","key":"15_CR49","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10009-023-00696-0","volume":"25","author":"J Scott","year":"2023","unstructured":"Scott, J., Niemetz, A., Preiner, M., Nejati, S., Ganesh, V.: Algorithm selection for SMT: MachSMT: Machine learning driven algorithm selection for SMT solvers. Int. J. Softw. Tools Technol. Transfer 25(2), 219\u2013239 (2023). https:\/\/doi.org\/10.1007\/s10009-023-00696-0","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"15_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Hunt, W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 127\u2013144. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-40922-X_8"},{"key":"15_CR51","unstructured":"Shervashidze, N., Schweitzer, P., van Leeuwen, E.J., Mehlhorn, K., Borgwardt, K.M.: Weisfeiler-Lehman graph kernels. J. Mach. Learn. Res. 12, 2539\u20132561 (2011). https:\/\/dl.acm.org\/doi\/10.5555\/1953048.2078187"},{"key":"15_CR52","unstructured":"Siglidis, G., Nikolentzos, G., Limnios, S., Giatsidis, C., Skianis, K., Vazirgiannis, M.: GraKeL: A graph kernel library in Python. J. Mach. Learn. Res. 21(54), 1\u20135 (2020). http:\/\/jmlr.org\/papers\/v21\/18-370.html"},{"key":"15_CR53","doi-asserted-by":"publisher","unstructured":"Su, Y., Yang, Q., Ci, Y.: Predicting lemmas in generalization of IC3. In: Proc. DAC. ACM (2024). https:\/\/doi.org\/10.1145\/3649329.3655970","DOI":"10.1145\/3649329.3655970"},{"key":"15_CR54","doi-asserted-by":"publisher","unstructured":"Tulsian, V., Kanade, A., Kumar, R., Lal, A., Nori, A.V.: MUX: Algorithm selection for software model checkers. In: Proc. MSR, pp. 132\u2013141. ACM (2014). https:\/\/doi.org\/10.1145\/2597073.2597080","DOI":"10.1145\/2597073.2597080"},{"key":"15_CR55","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1613\/JAIR.2490","volume":"32","author":"L Xu","year":"2008","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","journal-title":"J. Artif. Intell. Res."},{"key":"15_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-642-31612-8_18","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"L Xu","year":"2012","unstructured":"Xu, L., Hutter, F., Hoos, H., Leyton-Brown, K.: Evaluating component solver contributions to portfolio-based algorithm selectors. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 228\u2013241. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_18"}],"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-031-98668-0_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,27]],"date-time":"2026-04-27T15:08:46Z","timestamp":1777302526000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98668-0_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986673","9783031986680"],"references-count":56,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98668-0_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"22 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"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":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","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":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}