{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:17:20Z","timestamp":1767928640460,"version":"3.49.0"},"publisher-location":"Cham","reference-count":31,"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>Certification was made mandatory for the first time in the latest hardware model checking competition. In this case study, we investigate the trade-offs of requiring certificates for both passing and failing properties in the competition. Our evaluation shows that participating model checkers were able to produce compact, correct certificates that could be verified with minimal overhead. Furthermore, the certifying winner of the competition outperforms the previous non-certifying state-of-the-art model checker, demonstrating that certification can be adopted without compromising model checking efficiency.\n<\/jats:p>","DOI":"10.1007\/978-3-031-98668-0_14","type":"book-chapter","created":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T20:46:14Z","timestamp":1753130774000},"page":"281-295","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Introducing Certificates to\u00a0the\u00a0Hardware Model Checking Competition"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3925-3438","authenticated-orcid":false,"given":"Nils","family":"Froleyks","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4993-773X","authenticated-orcid":false,"given":"Emily","family":"Yu","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7142-6258","authenticated-orcid":false,"given":"Mathias","family":"Preiner","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7170-9242","authenticated-orcid":false,"given":"Armin","family":"Biere","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4547-2701","authenticated-orcid":false,"given":"Keijo","family":"Heljanko","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,22]]},"reference":[{"key":"14_CR1","unstructured":"Bacchus, F., Berg, J., J\u00e4rvisalo, M., Martins, R.: MaxSAT evaluation 2020: solver and benchmark descriptions (2020)"},{"key":"14_CR2","doi-asserted-by":"publisher","unstructured":"Beyer, D.: State of the art in software verification and witness validation: SV-COMP 2024. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) TACAS 2024. LNCS, vol. 14572, pp. 299\u2013329. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_15","DOI":"10.1007\/978-3-031-57256-2_15"},{"key":"14_CR3","doi-asserted-by":"publisher","unstructured":"Biere, A.: The AIGER And-Inverter Graph (AIG) format version 20071012. Technical report,\u00a007\/1, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2007). https:\/\/doi.org\/10.35011\/fmvtr.2007-1","DOI":"10.35011\/fmvtr.2007-1"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Biere, A., van Dijk, T., Heljanko, K.: Hardware model checking competition 2017. In: Stewart, D., Weissenbacher, G. (eds.) Formal Methods in Computer-Aided Design, FMCAD 2017, Vienna, Austria, 02\u201306 October 2017, p.\u00a09. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102233"},{"key":"14_CR5","doi-asserted-by":"publisher","unstructured":"Biere, A., Froleyks, N., Preiner, M.: Hardware model checking competition 2024. In: Narodytska, N., R\u00fcmmer, P. (eds.) Proceedings 24th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2024), 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":"14_CR6","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, Altenbergerstr. 69, 4040 Linz, Austria (2011). https:\/\/doi.org\/10.35011\/fmvtr.2011-2","DOI":"10.35011\/fmvtr.2011-2"},{"key":"14_CR7","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"},{"issue":"1","key":"14_CR8","doi-asserted-by":"publisher","first-page":"135","DOI":"10.3233\/SAT190106","volume":"9","author":"G Cabodi","year":"2014","unstructured":"Cabodi, G., et al.: Hardware model checking competition 2014: an analysis and comparison of solvers and benchmarks. J. Satisf. Boolean Model. Comput. 9(1), 135\u2013172 (2014). https:\/\/doi.org\/10.3233\/SAT190106","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-319-19249-9_9","volume-title":"FM 2015: Formal Methods","author":"S Conchon","year":"2015","unstructured":"Conchon, S., Mebsout, A., Za\u00efdi, F.: Certificates for parameterized model checking. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 126\u2013142. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-19249-9_9"},{"key":"14_CR10","doi-asserted-by":"publisher","unstructured":"Eriksson, S., Helmert, M.: Certified unsolvability for SAT planning with property directed reachability. In: Proceedings of the International Conference on Automated Planning and Scheduling, vol. 30, pp. 90\u2013100 (2020). https:\/\/doi.org\/10.1609\/icaps.v30i1.6649","DOI":"10.1609\/icaps.v30i1.6649"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Eriksson, S., R\u00f6ger, G., Helmert, M.: Unsolvability certificates for classical planning. In: Barbulescu, L., Frank, J., Mausam, Smith, S.F. (eds.) Proceedings of the Twenty-Seventh International Conference on Automated Planning and Scheduling, ICAPS 2017, Pittsburgh, Pennsylvania, USA, 18\u201323 June 2017, pp. 88\u201397. AAAI Press (2017)","DOI":"10.1609\/icaps.v27i1.13818"},{"key":"14_CR12","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. Arch. Formal Proofs 2014 (2014)","DOI":"10.1007\/978-3-642-39799-8_31"},{"key":"14_CR13","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2021.103572","volume":"301","author":"N Froleyks","year":"2021","unstructured":"Froleyks, N., Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M.: SAT competition 2020. Artif. Intell. 301, 103572 (2021)","journal-title":"Artif. Intell."},{"key":"14_CR14","doi-asserted-by":"publisher","unstructured":"Froleyks, N., Yu, E., Biere, A., Heljanko, K.: Certifying phase abstraction. In: Benzm\u00fcller, C., Heule, M.J.H., Schmidt, R.A. (eds.) IJCAR 2024. LNCS, vol. 14739, pp. 284\u2013303. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-63498-7_17","DOI":"10.1007\/978-3-031-63498-7_17"},{"issue":"2","key":"14_CR15","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). https:\/\/doi.org\/10.1007\/s10703-021-00369-1","journal-title":"Formal Methods Syst. Des."},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Ivrii, A.: K-induction without unrolling. In: 2017 Formal Methods in Computer Aided Design (FMCAD), pp. 148\u2013155. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102253"},{"key":"14_CR17","doi-asserted-by":"publisher","unstructured":"Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust Boolean reasoning for equivalence checking and functional property verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 21(12), 1377\u20131394 (2002). https:\/\/doi.org\/10.1109\/TCAD.2002.804386","DOI":"10.1109\/TCAD.2002.804386"},{"key":"14_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-319-03077-7_3","volume-title":"Hardware and Software: Verification and Testing","author":"T Kuismin","year":"2013","unstructured":"Kuismin, T., Heljanko, K.: Increasing confidence in liveness model checking results with proofs. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol. 8244, pp. 32\u201343. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-03077-7_3"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Mebsout, A., Tinelli, C.: Proof certificates for SMT-based model checkers for infinite-state systems. In: FMCAD, pp. 117\u2013124. IEEE (2016)","DOI":"10.1109\/FMCAD.2016.7886669"},{"key":"14_CR20","doi-asserted-by":"publisher","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R.K.: DAG-aware AIG rewriting a fresh look at combinational logic synthesis. In: Sentovich, E. (ed.) Proceedings of the 43rd Design Automation Conference, DAC 2006, San Francisco, CA, USA, 24\u201328 July 2006, pp. 532\u2013535. ACM (2006). https:\/\/doi.org\/10.1145\/1146909.1147048","DOI":"10.1145\/1146909.1147048"},{"key":"14_CR21","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":"14_CR22","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":"14_CR23","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"14_CR24","unstructured":"Paulson, L., Nipkow, T.: The Sledgehammer: let automatic theorem provers write your Isabelle scripts (2023)"},{"key":"14_CR25","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1016\/j.artint.2019.04.002","volume":"274","author":"L Pulina","year":"2019","unstructured":"Pulina, L., Seidl, M.: The 2016 and 2017 QBF solvers evaluations (QBFEVAL\u201916 and QBFEVAL\u201917). Artif. Intell. 274, 224\u2013248 (2019)","journal-title":"Artif. Intell."},{"key":"14_CR26","unstructured":"Sutcliffe, G.: Proceedings of the 12th IJCAR ATP System Competition (CASC-J12) (2024)"},{"issue":"1","key":"14_CR27","doi-asserted-by":"publisher","first-page":"221","DOI":"10.3233\/SAT190123","volume":"11","author":"T Weber","year":"2019","unstructured":"Weber, T., Conchon, S., D\u00e9harbe, D., Heizmann, M., Niemetz, A., Reger, G.: The SMT competition 2015\u20132018. J. Satisfiability Boolean Model. Comput. 11(1), 221\u2013259 (2019)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"14_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-319-09284-3_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"N Wetzler","year":"2014","unstructured":"Wetzler, N., Heule, M., Hunt, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422\u2013429. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_31"},{"key":"14_CR29","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. (eds.) CAV 2021. LNCS, vol. 12760, pp. 363\u2013386. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_17"},{"key":"14_CR30","doi-asserted-by":"publisher","unstructured":"Yu, E., Froleyks, N., Biere, A., Heljanko, K.: Stratified certification for K-Induction. In: Griggio, A., Rungta, N. (eds.) 22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, 17\u201321 October 2022, pp. 59\u201364. IEEE (2022). https:\/\/doi.org\/10.34727\/2022\/ISBN.978-3-85448-053-2_11","DOI":"10.34727\/2022\/ISBN.978-3-85448-053-2_11"},{"key":"14_CR31","doi-asserted-by":"publisher","unstructured":"Yu, E., Froleyks, N., Biere, A., Heljanko, K.: Towards compositional hardware model checking certification. In: Nadel, A., Rozier, K.Y. (eds.) Formal Methods in Computer-Aided Design, FMCAD 2023, Ames, IA, USA, 24\u201327 October 2023, pp. 1\u201311. IEEE (2023). https:\/\/doi.org\/10.34727\/2023\/ISBN.978-3-85448-060-0_12","DOI":"10.34727\/2023\/ISBN.978-3-85448-060-0_12"}],"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_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,18]],"date-time":"2025-10-18T05:38:32Z","timestamp":1760765912000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98668-0_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986673","9783031986680"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98668-0_14","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":"The authors have no competing interests to declare that are relevant to the content of this paper.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"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"}}]}}