{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:00:07Z","timestamp":1779087607996,"version":"3.51.4"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030816872","type":"print"},{"value":"9783030816889","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T00:00:00Z","timestamp":1626307200000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a formal framework to certify<jats:italic>k<\/jats:italic>-induction-based model checking results. The key idea is the notion of a<jats:italic>k<\/jats:italic>-witness circuit which simulates the given circuit and has a simple inductive invariant serving as proof certificate. Our approach allows to check proofs with an independent proof checker by reducing the certification problem to pure SAT checks and checking a simple QBF with one quantifier alternation. We also present<jats:sc>Certifaiger<\/jats:sc>, the resulting certification toolkit, and evaluate it on instances from the hardware model checking competition. Our experiments show the practical use of our certification method.<\/jats:p>","DOI":"10.1007\/978-3-030-81688-9_17","type":"book-chapter","created":{"date-parts":[[2021,7,16]],"date-time":"2021-07-16T16:20:47Z","timestamp":1626452447000},"page":"363-386","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Progress in Certifying Hardware Model Checking Results"],"prefix":"10.1007","author":[{"given":"Emily","family":"Yu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Keijo","family":"Heljanko","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"17_CR1","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. In: LICS, pp. 165\u2013175. IEEE Computer Society (1988)"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Balyo, T., Heule, M.J.H., J\u00e4rvisalo, M.: SAT competition 2016: recent developments. In: Singh, S.P., Markovitch, S. (eds.) Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, pp. 5061\u20135063. AAAI Press (2017)","DOI":"10.1609\/aaai.v31i1.10641"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Biere, A., Brummayer, R.: Consistency checking of all different constraints over bit-vectors within a SAT solver. In: FMCAD, pp. 1\u20134. IEEE (2008)","DOI":"10.1109\/FMCAD.2008.ECP.32"},{"key":"17_CR4","unstructured":"Biere, A., Claessen, K.: Hardware model checking competition 2010 (2010). http:\/\/fmv.jku.at\/hwmcc10\/"},{"key":"17_CR5","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, p. 9. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102233"},{"key":"17_CR6","unstructured":"Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT competition 2020. In: Balyo, T., Froleyks, N., Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proc. of SAT Competition 2020 - Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2020-1, pp. 51\u201353. University of Helsinki (2020)"},{"key":"17_CR7","unstructured":"Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Tech. rep. 11\/2, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2011)"},{"key":"17_CR8","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":"17_CR9","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"},{"issue":"3","key":"17_CR10","first-page":"36:1","volume":"18","author":"G Cabodi","year":"2013","unstructured":"Cabodi, G., Nocco, S., Quer, S.: Thread-based multi-engine model checking for multicore platforms. ACM Trans. Des. Autom. Electr. Syst. 18(3), 36:1\u201336:28 (2013)","journal-title":"ACM Trans. Des. Autom. Electr. Syst."},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Case, M.L., Mony, H., Baumgartner, J., Kanzelman, R.: Enhanced verification by temporal decomposition. In: FMCAD, pp. 17\u201324. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351146"},{"key":"17_CR12","unstructured":"Certifaiger: Certifaiger (2021). http:\/\/fmv.jku.at\/certifaiger"},{"key":"17_CR13","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":"17_CR14","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":"17_CR15","doi-asserted-by":"crossref","unstructured":"Degtyarev, A., Voronkov, A.: Equality reasoning in sequent-based calculi. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 611\u2013706. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50012-6"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-642-23702-7_26","volume-title":"Static Analysis","author":"AF Donaldson","year":"2011","unstructured":"Donaldson, A.F., Haller, L., Kroening, D., R\u00fcmmer, P.: Software verification using k-induction. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 351\u2013368. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23702-7_26"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/11499107_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2005","unstructured":"E\u00e9n, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61\u201375. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11499107_5"},{"issue":"4","key":"17_CR18","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1016\/S1571-0661(05)82542-3","volume":"89","author":"N E\u00e9n","year":"2003","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal induction by incremental SAT solving. Electron. Notes Theor. Comput. Sci. 89(4), 543\u2013560 (2003)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-96142-2_3","volume-title":"Computer Aided Verification","author":"A Gacek","year":"2018","unstructured":"Gacek, A., Backes, J., Whalen, M., Wagner, L., Ghassabani, E.: The JKind model checker. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 20\u201327. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_3"},{"issue":"4","key":"17_CR20","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/s10009-017-0475-0","volume":"20","author":"N Ge","year":"2018","unstructured":"Ge, N., Jenn, E., Breton, N., Fonteneau, Y.: Integrated formal verification of safety-critical software. Int. J. Softw. Tools Technol. Transf. 20(4), 423\u2013440 (2018)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Griggio, A., Roveri, M., Tonetta, S.: Certifying proofs for LTL model checking. In: FMCAD, pp. 1\u20139. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8603022"},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"Gro\u00dfe, D., Le, H.M., Drechsler, R.: Induction-based formal verification of SystemC TLM designs. In: MTV, pp. 101\u2013106. IEEE Computer Society (2009)","DOI":"10.1109\/MTV.2009.16"},{"key":"17_CR23","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"},{"issue":"1","key":"17_CR24","first-page":"133","volume":"11","author":"MJH Heule","year":"2019","unstructured":"Heule, M.J.H., J\u00e4rvisalo, M., Suda, M.: SAT competition 2018. J. Satisf. Boolean Model. Comput. 11(1), 133\u2013154 (2019)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"17_CR25","unstructured":"Jordan, C., Klieber, W., Seidl, M.: Non-cnf QBF solving with QCIR. In: AAAI Workshop: Beyond NP. AAAI Workshops, vol. WS-16-05. AAAI Press (2016)"},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"Jovanovic, D., Dutertre, B.: Property-directed k-induction. In: FMCAD, pp. 85\u201392. IEEE (2016)","DOI":"10.1109\/FMCAD.2016.7886665"},{"key":"17_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-030-25543-5_21","volume-title":"Computer Aided Verification","author":"HG Vediramana Krishnan","year":"2019","unstructured":"Vediramana Krishnan, H.G., Vizel, Y., Ganesh, V., Gurfinkel, A.: Interpolating strong induction. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 367\u2013385. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_21"},{"key":"17_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/3-540-44585-4_10","volume-title":"Computer Aided Verification","author":"A Kuehlmann","year":"2001","unstructured":"Kuehlmann, A., Baumgartner, J.: Transformation-based verification using generalized retiming. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 104\u2013117. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_10"},{"key":"17_CR29","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":"17_CR30","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1016\/j.ress.2012.03.021","volume":"105","author":"J Lahtinen","year":"2012","unstructured":"Lahtinen, J., Valkonen, J., Bj\u00f6rkman, K., Frits, J., Niemel\u00e4, I., Heljanko, K.: Model checking of safety-critical software in the nuclear engineering domain. Reliab. Eng. Syst. Saf. 105, 104\u2013113 (2012)","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"17_CR31","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Brayton, R.K.: Recording synthesis history for sequential verification. In: FMCAD, pp. 1\u20138. IEEE (2008)","DOI":"10.1109\/FMCAD.2008.ECP.8"},{"key":"17_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/978-3-540-27813-9_45","volume-title":"Computer Aided Verification","author":"L de Moura","year":"2004","unstructured":"de Moura, L., et al.: SAL 2. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 496\u2013500. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_45"},{"key":"17_CR33","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":"17_CR34","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":"17_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/978-3-319-40970-2_24","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"L Tentrup","year":"2016","unstructured":"Tentrup, L.: Non-prenex QBF solving using abstraction. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 393\u2013401. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_24"},{"key":"17_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-319-57288-8_29","volume-title":"NASA Formal Methods","author":"L Wagner","year":"2017","unstructured":"Wagner, L., Mebsout, A., Tinelli, C., Cofer, D., Slind, K.: Qualification of a model checker for avionics software verification. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 404\u2013419. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-57288-8_29"},{"key":"17_CR37","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"}],"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-030-81688-9_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,4]],"date-time":"2023-01-04T17:46:30Z","timestamp":1672854390000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81688-9_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816872","9783030816889"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81688-9_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"15 July 2021","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":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"290","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"63","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers and 5 invited papers are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}