{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:03:17Z","timestamp":1784793797143,"version":"3.55.0"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325181","type":"print"},{"value":"9783032325198","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>The IC3 algorithm represents the state-of-the-art (SOTA) hardware model checking technique, owing to its robust performance and scalability. A significant body of research has focused on enhancing the solving efficiency of the IC3 algorithm, with particular attention to the inductive generalization process\u2014a critical phase wherein the algorithm seeks to generalize a counterexample to inductiveness (CTI), which typically is a state leading to a bad state, into a broader set of states. This inductive generalization is a primary source of clauses in\u00a0IC3 and thus plays a pivotal role in determining the overall effectiveness of the algorithm.<\/jats:p>\n                  <jats:p>Despite its importance, existing approaches often rely on fixed inductive generalization strategies, overlooking the dynamic and context-sensitive nature of the verification environment in which spurious counterexamples arise. This rigidity can limit the quality of generated clauses and, consequently, the performance of IC3.<\/jats:p>\n                  <jats:p>To address this limitation, we propose a lightweight machine-learning-based framework that dynamically selects appropriate inductive generalization strategies in response to the evolving verification context. Specifically, we employ a multi-armed bandit (MAB) algorithm to adaptively choose inductive generalization strategies based on real-time feedback from the verification process. The agent is updated by evaluating the quality of generalization outcomes, thereby refining its strategy selection over time.<\/jats:p>\n                  <jats:p>Empirical evaluation on a benchmark suite comprising 914 instances, primarily drawn from the latest HWMCC collection, demonstrates the efficacy of our approach. When implemented on the state-of-the-art model checker rIC3, our method solves 26 to 50 more cases than the baselines and improves the PAR-2 score by 194.72 to 389.29.<\/jats:p>","DOI":"10.1007\/978-3-032-32519-8_19","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:17:26Z","timestamp":1784791046000},"page":"357-379","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["$$\\mathcal {A}\\text {-} \\texttt {IC3}$$: Learning-Guided Adaptive Inductive Generalization for\u00a0Hardware Model Checking"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5878-3683","authenticated-orcid":false,"given":"Xiaofeng","family":"Zhou","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5077-8361","authenticated-orcid":false,"given":"Guangyu","family":"Hu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4001-264X","authenticated-orcid":false,"given":"Hongce","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7622-6714","authenticated-orcid":false,"given":"Wei","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"19_CR1","doi-asserted-by":"publisher","unstructured":"Biere, A., Cimatti, A., Clarke, E., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proceedings 1999 Design Automation Conference (Cat. No. 99CH36361), pp. 317\u2013320 (1999). https:\/\/doi.org\/10.1109\/DAC.1999.781333","DOI":"10.1109\/DAC.1999.781333"},{"key":"19_CR2","unstructured":"Biere, A., Froleyks, N., Preiner, M.: HWMCC\u201920 Benchmarks (2020). https:\/\/fmv.jku.at\/hwmcc20\/hwmcc20benchmarks.tar.xz, benchmark archive for the Hardware Model Checking Competition 2020 (BTOR2 and bit-blasted AIGER formats)"},{"key":"19_CR3","doi-asserted-by":"publisher","unstructured":"Biere, A., Froleyks, N., Preiner, M.: Hardware model checking competition 2024. In: 2024 Formal Methods in Computer-Aided Design (FMCAD), p. 1 (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":"19_CR4","doi-asserted-by":"publisher","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) Verification, Model Checking, and Abstract Interpretation. VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Berlin, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"19_CR5","doi-asserted-by":"publisher","unstructured":"Cherif, M.S., Habet, D., Terrioux, C.: Combining VSIDS and CHB using restarts in SAT. In: Michel, L.D. (ed.) 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0210, pp. 20:1\u201320:19. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2021). https:\/\/doi.org\/10.4230\/LIPIcs.CP.2021.20","DOI":"10.4230\/LIPIcs.CP.2021.20"},{"key":"19_CR6","unstructured":"Een, N., Mishchenko, A., Brayton, R.: Efficient implementation of property directed reachability. In: 2011 Formal Methods in Computer-Aided Design (FMCAD), pp. 125\u2013134 (2011). https:\/\/dl.acm.org\/doi\/10.5555\/2157654.2157675"},{"key":"19_CR7","doi-asserted-by":"publisher","unstructured":"Hassan, Z., Bradley, A.R., Somenzi, F.: Better generalization in ic3. In: 2013 Formal Methods in Computer-Aided Design, pp. 157\u2013164 (2013). https:\/\/doi.org\/10.1109\/FMCAD.2013.6679405","DOI":"10.1109\/FMCAD.2013.6679405"},{"key":"19_CR8","doi-asserted-by":"publisher","unstructured":"Hu, G., Tang, J., Yu, C., Zhang, W., Zhang, H.: DeepIC3: guiding IC3 algorithms by graph neural network clause prediction. In: 2024 29th Asia and South Pacific Design Automation Conference (ASP-DAC), pp. 262\u2013268 (2024). https:\/\/doi.org\/10.1109\/ASP-DAC58780.2024.10473807","DOI":"10.1109\/ASP-DAC58780.2024.10473807"},{"key":"19_CR9","doi-asserted-by":"publisher","unstructured":"Hu, G., Zhang, W., Zhang, H.: NeuroPDR: integrating neural networks in the pdr algorithm for hardware model checking. In: 2023 ACM\/IEEE 5th Workshop on Machine Learning for CAD (MLCAD), pp.\u00a01\u20136 (2023). https:\/\/doi.org\/10.1109\/MLCAD58807.2023.10299875","DOI":"10.1109\/MLCAD58807.2023.10299875"},{"key":"19_CR10","unstructured":"Jakub\u016fv, J., Janota, M., Piotrowski, B., Piepenbrock, J., Reynolds, A.: Selecting quantifiers for instantiation in SMT. In: Proceedings of the 21st International Workshop on Satisfiability Modulo Theories (SMT 2023). CEUR Workshop Proceedings, vol.\u00a03429, pp. 71\u201377. CEUR-WS.org (2023). https:\/\/ceur-ws.org\/Vol-3429\/short10.pdf"},{"key":"19_CR11","doi-asserted-by":"publisher","unstructured":"Le, N., Si, X., Gurfinkel, A.: Data-driven optimization of inductive generalization. In: FMCAD, pp. 86\u201395 (2021). https:\/\/doi.org\/10.34727\/2021\/isbn.978-3-85448-046-4_17","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_17"},{"key":"19_CR12","doi-asserted-by":"publisher","unstructured":"Li, L., Chu, W., Langford, J., Schapire, R.E.: A contextual-bandit approach to personalized news article recommendation. In: Proceedings of the 19th International Conference on World Wide Web, pp. 661\u2013670. ACM (2010). https:\/\/doi.org\/10.1145\/1772690.1772758","DOI":"10.1145\/1772690.1772758"},{"key":"19_CR13","doi-asserted-by":"publisher","unstructured":"Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Exponential recency weighted average branching heuristic for SAT solvers. In: Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, pp. 3434\u20133440 (2016). https:\/\/doi.org\/10.1609\/aaai.v30i1.10439","DOI":"10.1609\/aaai.v30i1.10439"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-319-40970-2_9","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"JH Liang","year":"2016","unstructured":"Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 123\u2013140. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_9"},{"key":"19_CR15","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":"19_CR16","doi-asserted-by":"publisher","unstructured":"Preiner, M., Froleyks, N., Biere, A.: HWMCC\u201924 Benchmarks and Results. https:\/\/doi.org\/10.5281\/zenodo.14156844, https:\/\/zenodo.org\/records\/14156844","DOI":"10.5281\/zenodo.14156844"},{"key":"19_CR17","doi-asserted-by":"publisher","unstructured":"Preiner, M., Froleyks, N., Biere, A.: HWMCC\u201925 Benchmarks and Results (2025).https:\/\/doi.org\/10.5281\/zenodo.17428464, https:\/\/zenodo.org\/records\/17428464, dataset, version v1, published 2025-10-23","DOI":"10.5281\/zenodo.17428464"},{"key":"19_CR18","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":"19_CR19","doi-asserted-by":"crossref","unstructured":"Su, Y., Yang, Q., Ci, Y., Bu, T., Huang, Z.: The rIC3 hardware model checker (2025). https:\/\/arxiv.org\/abs\/2502.13605","DOI":"10.1007\/978-3-031-98668-0_9"},{"key":"19_CR20","unstructured":"Su, Y., Yang, Q., Ci, Y., Huang, Z.: Extended ctg generalization and dynamic adjustment of generalization strategies in ic3 (2025). https:\/\/arxiv.org\/abs\/2501.02480"},{"key":"19_CR21","doi-asserted-by":"publisher","unstructured":"Vediramana\u00a0Krishnan, H.G., Chen, Y., Shoham, S., Gurfinkel, A.: Global guidance for local generalization in model checking. Form. Methods Syst. Des. 63(1), 81\u2013109 (2024). https:\/\/doi.org\/10.1007\/s10703-023-00412-3","DOI":"10.1007\/s10703-023-00412-3"},{"key":"19_CR22","doi-asserted-by":"publisher","unstructured":"VK, H.G., Fedyukovich, G., Gurfinkel, A.: Word level property directed reachability. In: 2020 IEEE\/ACM International Conference On Computer Aided Design (ICCAD), pp.\u00a01\u20139. IEEE (2020). https:\/\/doi.org\/10.1145\/3400302.3415708","DOI":"10.1145\/3400302.3415708"},{"key":"#cr-split#-19_CR23.1","unstructured":"Winterer, F., Seufert, T., Scheibler, K., Teige, T., Scholl, C., Becker, B.: ICP and IC3 with stronger generalization. In: MBMV 2021"},{"key":"#cr-split#-19_CR23.2","unstructured":"24th Workshop, pp. 1-12. VDE (2021). https:\/\/abs.informatik.uni-freiburg.de\/papers\/2021\/WSS+_2021.pdf"}],"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-32519-8_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:17:29Z","timestamp":1784791049000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32519-8_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325181","9783032325198"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32519-8_19","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\u00a0the 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"}}]}}