{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T16:08:07Z","timestamp":1779034087364,"version":"3.51.4"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262035","type":"print"},{"value":"9783032262042","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,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"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                    Model checking is a powerful automated reasoning technique for verifying hardware designs, ensuring that they function correctly before deployment. However, modern model checkers are complex software systems with hundreds of thousands of lines of code, making them prone to errors. To increase confidence in verification results, recent efforts in hardware verification focus on requiring model checkers to produce machine-checkable proofs according to a standardized format that can be independently validated. Yet, implementing proof generation across different verification algorithms presents a unique challenge. In hardware model checking, constraints play an essential role, as they encode assumptions about the environment and help simplify analysis. This paper addresses the challenge by developing a certification approach that ensures verification results remain trustworthy when constraints are present. We introduce certificate generation methods for three classes of constraints that can be extracted from the models. Furthermore, to support a broader range of constraints and more complex reset logic for industrial use, we also provide alternative Quantified Boolean Formula checks in the proof format with a single quantifier alternation. Lastly, we present a certificate generation method for\n                    <jats:italic>k<\/jats:italic>\n                    -induction with uniqueness constraints, an important model checking technique. We implement these in a certification toolkit, and provide empirical evaluation on competition benchmarks, demonstrating their effectiveness.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-26204-2_9","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T15:50:56Z","timestamp":1779033056000},"page":"170-188","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Certifying Constraints in\u00a0Hardware Model Checking"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3925-3438","authenticated-orcid":false,"given":"Nils","family":"Froleyks","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4993-773X","authenticated-orcid":false,"given":"Emily","family":"Yu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7170-9242","authenticated-orcid":false,"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4547-2701","authenticated-orcid":false,"given":"Keijo","family":"Heljanko","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M., Stahlbauer, A.: Witness validation and stepwise testification across software verifiers. In: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, pp. 721\u2013733 (2015)","DOI":"10.1145\/2786805.2786867"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus. J.-G.: A fully verified executable LTL model checker (2014)","DOI":"10.1007\/978-3-642-39799-8_31"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-030-81688-9_17","volume-title":"Computer Aided Verification","author":"E Yu","year":"2021","unstructured":"Yu, E., Biere, A., Heljanko, K.: Progress in certifying hardware model checking results. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 363\u2013386. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_17"},{"issue":"2","key":"9_CR4","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/s10703-021-00369-1","volume":"57","author":"A Griggio","year":"2021","unstructured":"Griggio, A., Roveri, M., Tonetta, S.: Certifying proofs for SAT-based model checking. Formal Methods Syst. Des. 57(2), 178\u2013210 (2021)","journal-title":"Formal Methods Syst. Des."},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-44585-4_2","volume-title":"Computer Aided Verification","author":"KS Namjoshi","year":"2001","unstructured":"Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 2\u201313. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_2"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/BFb0028768","volume-title":"Computer Aided Verification","author":"M Kaufman","year":"1998","unstructured":"Kaufman, M., Martin, A., Pixley, C.: Design constraints in symbolic model checking. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 477\u2013487. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0028768"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Hollander, Y., Morley, M., Noy, A.: The e language: a fresh separation of concerns. In: Proceedings Technology of Object-Oriented Languages and Systems. TOOLS, vol. 38, pp. 41\u201350. IEEE (2001)","DOI":"10.1109\/TOOLS.2001.911754"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A.: Reactive modules. Formal Methods Syst. Des. 15, 7\u201348 (1999)","DOI":"10.1023\/A:1008739929481"},{"key":"9_CR9","unstructured":"Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond (2011)"},{"key":"9_CR10","unstructured":"Biere, A., Froleyks, N., Preiner, M.: Hardware model checking competition 2024. In: FMCAD, p. 7. TU Wien Academic Press (2024)"},{"key":"9_CR11","doi-asserted-by":"publisher","unstructured":"Froleyks, N., Yu, E., Preiner, M., Biere, A., Heljanko, K.: Introducing certificates to the hardware model checking competition. In: Piskac, R., Rakamari\u0107, Z. (eds.) Computer Aided Verification. CAV 2025. Lecture Notes in Computer Science, vol. 15931, pp. 281\u2013295. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-98668-0_14","DOI":"10.1007\/978-3-031-98668-0_14"},{"key":"9_CR12","unstructured":"Yu, E., Froleyks, N., Biere, A., Heljanko, K.: Stratified certification for K-induction. In: FMCAD, pp. 59\u201364. IEEE (2022)"},{"issue":"7","key":"9_CR13","doi-asserted-by":"publisher","first-page":"950","DOI":"10.1109\/43.293952","volume":"13","author":"S Malik","year":"1994","unstructured":"Malik, S.: Analysis of cyclic combinational circuits. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 13(7), 950\u2013956 (1994)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Jiang, J-HR., Mishchenko, A., Brayton, R.K.: On breakable cyclic definitions. In: IEEE\/ACM International Conference on Computer Aided Design, 2004. ICCAD-2004, pp. 411\u2013418. IEEE (2004)","DOI":"10.1109\/ICCAD.2004.1382610"},{"key":"9_CR15","unstructured":"Riedel, M.D.: Cyclic combinational circuits. California Institute of Technology (2004)"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Cabodi, G., Camurati, P., Garcia, L.A., Murciano, M., Nocco, S., Quer, S:. Speeding up model checking by exploiting explicit and hidden verification constraints. In: DATE, pp. 1686\u20131691. IEEE (2009)","DOI":"10.1109\/DATE.2009.5090934"},{"key":"9_CR17","unstructured":"Koen Claessen, K., S\u00f6rensson, N.: A liveness checking algorithm that counts. In: FMCAD, pp. 52\u201359. IEEE (2012)"},{"key":"9_CR18","doi-asserted-by":"publisher","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","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Jahanpour, M.S., and Mohamed, O.A.: Automatic generation of model checking properties and constraints from production based specification. In: The 2004 47th Midwest Symposium on Circuits and Systems, 2004. MWSCAS\u201904, vol.\u00a03, pp. iii\u2013435. IEEE (2004)","DOI":"10.1109\/MWSCAS.2004.1354388"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Yuan, J., Albin, K., Aziz, A., Pixley, C.: Constraint synthesis for environment modeling in functional verification. In: Proceedings of the 40th Annual Design Automation Conference, pp. 296\u2013299 (2003)","DOI":"10.1145\/775832.775909"},{"key":"9_CR21","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":"9_CR22","unstructured":"Yu, Z.E.: Certifying hardware model checking\/submitted by Emily Zhengqi Yu (2023)"},{"key":"9_CR23","unstructured":"Yu, E., Froleyks, N., Biere, A., Heljanko, K.: Towards compositional hardware model checking certification. In: FMCAD, pp. 1\u201311. IEEE (2023)"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Goldberg, E., G\u00fcdemann, M., Kroening, D., Mukherjee, R.: Efficient verification of multi-property designs (the benefit of wrong assumptions). In: 2018 Design, Automation & Test in Europe Conference & Exhibition (DATE), pp. 43\u201348 (2018)","DOI":"10.23919\/DATE.2018.8341977"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Das, S., Hazra, A., Dasgupta, P., Kundu, S., Jain, H.: Purse: property ordering using runtime statistics for efficient multi - property verification. In: 2024 Design, Automation & Test in Europe Conference & Exhibition (DATE), pp. 1\u20136 (2024)","DOI":"10.23919\/DATE58400.2024.10546895"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-31612-8_1","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"AR Bradley","year":"2012","unstructured":"Bradley, A.R.: Understanding IC3. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 1\u201314. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_1"},{"key":"9_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/3-540-40922-X_23","volume-title":"Formal Methods in Computer-Aided Design","author":"P Bjesse","year":"2000","unstructured":"Bjesse, P., Claessen, K.: SAT-based verification without state space traversal. In: Hunt, W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 409\u2013426. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-40922-X_23"},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1007\/978-3-030-32409-4_32","volume-title":"Formal Methods and Software Engineering","author":"Z Yu","year":"2019","unstructured":"Yu, Z., Biere, A., Heljanko, K.: Certifying hardware model checking results. In: Ait-Ameur, Y., Qin, S. (eds.) ICFEM 2019. LNCS, vol. 11852, pp. 498\u2013502. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32409-4_32"},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Ivrii, A.: K-induction without unrolling. In: FMCAD, pp. 148\u2013155. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102253"},{"key":"9_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-319-23534-9_2","volume-title":"Fields of Logic and Computation II","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24\u201351. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23534-9_2"},{"key":"9_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"510","DOI":"10.1007\/978-3-319-41540-6_29","volume-title":"Computer Aided Verification","author":"A Champion","year":"2016","unstructured":"Champion, A., Mebsout, A., Sticksel, C., Tinelli, C.: The kind 2 model checker. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 510\u2013517. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_29"},{"key":"9_CR32","doi-asserted-by":"crossref","unstructured":"Biere, A., Brummayer, R.: Consistency checking of all different constraints over bit-vectors within a SAT solver. In: 2008 Formal Methods in Computer-Aided Design, pp. 1\u20134. IEEE (2008)","DOI":"10.1109\/FMCAD.2008.ECP.32"},{"key":"9_CR33","unstructured":"Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., Pollitt, F.: CaDiCaL, Gimsatul, IsaSAT and Kissat entering the SAT Competition 2024. In: Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M.(eds.) Proceedings of SAT Competition 2024 \u2013 Solver, Benchmark and Proof Checker Descriptions, vol. B-2024-1 of Department of Computer Science Report Series B, pp. 8\u201310. University of Helsinki (2024)"},{"issue":"1","key":"9_CR34","doi-asserted-by":"publisher","first-page":"155","DOI":"10.3233\/SAT190121","volume":"11","author":"L Tentrup","year":"2019","unstructured":"Tentrup, L.: CAQE and QuAbS: abstraction based QBF solvers. J. Satisfiability Boolean Model. Comput. 11(1), 155\u2013210 (2019)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"9_CR35","unstructured":"Jordan, C., Klieber, W., Seidl, M.: Non-CNF QBF solving with QCIR. In: AAAI Workshop: Beyond NP, vol. WS-16-05 of AAAI Technical Report. AAAI Press (2016)"},{"key":"9_CR36","doi-asserted-by":"publisher","unstructured":"Froleyks, N., Yu, E., Biere, A., Heljanko, K.: Certifying phase abstraction. In: Benzm\u00fcller, C., Heule, M.J., Schmidt, R.A. (eds) Automated Reasoning. IJCAR 2024. Lecture Notes in Computer Science(), vol. 14739. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-63498-7_17","DOI":"10.1007\/978-3-031-63498-7_17"},{"key":"9_CR37","unstructured":"Biere, A., Fazekas, K., Fleury, M., Froleyks, N.: Clausal congruence closure. In: 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik (2024)"},{"key":"9_CR38","doi-asserted-by":"crossref","unstructured":"Shenoy, N., Rudell, R.: Efficient implementation of retiming. The Best of ICCAD: 20 Years of Excellence in Computer-Aided Design, pp. 615\u2013630 (2003)","DOI":"10.1007\/978-1-4615-0292-0_49"}],"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-032-26204-2_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T15:50:59Z","timestamp":1779033059000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26204-2_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262035","9783032262042"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26204-2_9","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":"18 May 2026","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":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","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":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}