{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:11:45Z","timestamp":1784837505122,"version":"3.55.0"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031999833","type":"print"},{"value":"9783031999840","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,30]],"date-time":"2025-07-30T00:00:00Z","timestamp":1753833600000},"content-version":"vor","delay-in-days":210,"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>In the field of formal verification, certifying proofs serve as compelling evidence to demonstrate the correctness of a model within a deductive system. These proofs can be automatically generated as a by-product of the verification process and are key artifacts for high-assurance systems. Their significance lies in their ability to be independently verified by proof checkers, which provides a more convenient approach than certifying the tools that generate them. Modern model checking algorithms adopt deductive methods and usually generate proofs in terms of inductive invariants, assuming that these apply to the original system under verification. Model checkers, though, often make use of a range of complex pre-processing simplifications and transformations to ease the verification process, which add another layer of complexity to the generation of proofs. In this paper, we present a novel approach for certifying model checking results exploiting a theorem prover and a theory of temporal deductive rules that can support various kinds of transformations and simplification of the original circuit. We implemented and experimentally evaluated our contribution on invariants generated using two state-of-the-art model checkers, nuXmv and PdTRAV, and by defining a set of rules within a theorem prover, to validate each certificate.<\/jats:p>","DOI":"10.1007\/978-3-031-99984-0_24","type":"book-chapter","created":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:47:48Z","timestamp":1753789668000},"page":"449-467","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["A Theorem Prover Based Approach for\u00a0SAT-Based Model Checking Certification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4003-2317","authenticated-orcid":false,"given":"Giulia","family":"Sindoni","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6233-0994","authenticated-orcid":false,"given":"Paolo","family":"Pasini","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5839-8697","authenticated-orcid":false,"given":"Gianpiero","family":"Cabodi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2476-2160","authenticated-orcid":false,"given":"Paolo E.","family":"Camurati","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3311-0893","authenticated-orcid":false,"given":"Alberto","family":"Griggio","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0605-9014","authenticated-orcid":false,"given":"Marco","family":"Palena","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9483-3940","authenticated-orcid":false,"given":"Marco","family":"Roveri","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9091-7899","authenticated-orcid":false,"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,7,30]]},"reference":[{"issue":"1","key":"24_CR1","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1023\/A:1024485130001","volume":"23","author":"J Baumgartner","year":"2003","unstructured":"Baumgartner, J., Heyman, T., Singhal, V., Aziz, A.: An abstraction algorithm for the verification of level-sensitive latch-based netlists. Form. Methods Syst. Des. 23(1), 39\u201365 (2003)","journal-title":"Form. Methods Syst. Des."},{"key":"24_CR2","unstructured":"Biere, A., Jussila, T.: The model checking competition web page, http:\/\/fmv.jku.at\/hwmcc"},{"issue":"2","key":"24_CR3","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1016\/S1571-0661(04)80410-9","volume":"66","author":"A Biere","year":"2002","unstructured":"Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. Electron. Notes Theor. Comput. Sci. 66(2), 160\u2013177 (2002)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"24_CR4","unstructured":"Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Technical Report 11\/2, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2011)"},{"key":"24_CR5","unstructured":"Biere, A., Yu, E., Froleyks, N.: Stratified certification for k-induction. In: Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design\u2013FMCAD 2022, vol.\u00a03, p.\u00a059. TU Wien Academic Press (2022)"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Bjesse, P., Kukula, J.: Automatic generalized phase abstraction for formal verification. In: ICCAD-2005. IEEE\/ACM International Conference on Computer-Aided Design, vol. 2005, pp. 1076\u20131082. IEEE (2005)","DOI":"10.1109\/ICCAD.2005.1560220"},{"key":"24_CR7","unstructured":"Boulton, R.J., et al.: Experience with embedding hardware description languages in hol. In: TPCD, vol.\u00a010, pp. 129\u2013156 (1992)"},{"key":"24_CR8","unstructured":"Bradley, A.R., Somenzi, F., Hassan, Z., Zhang, Y.: An incremental approach to model checking progress properties. In: 2011 Formal Methods in Computer-Aided Design (FMCAD), pp. 144\u2013153. IEEE (2011)"},{"issue":"1","key":"24_CR9","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/s10703-017-0272-0","volume":"50","author":"G Cabodi","year":"2017","unstructured":"Cabodi, G., Camurati, P.E., Mishchenko, A., Palena, M., Pasini, P.: SAT solver management strategies in IC3: an experimental approach. Form. Methods Syst. Des. 50(1), 39\u201374 (2017)","journal-title":"Form. Methods Syst. Des."},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"Cabodi, G., Palena, M., Pasini, P.: Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking. Formal Methods Syst. Des. 60(2), 117\u2013146 (2022)","DOI":"10.1007\/s10703-022-00406-7"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"Cabodi, G., Camurati, P.E., Palena, M., Pasini, P., Vendraminetto, D.: Logic synthesis for interpolant circuit compaction. IEEE Trans. Comput.-Aided Des. Integr. Circ. Syst. 38(2), 380\u2013384 (2018)","DOI":"10.1109\/TCAD.2018.2808229"},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"Cabodi, G., Camurati, P.E., Palena, M., Pasini, P., Vendraminetto, D.: Reducing interpolant circuit size through SAT-based weakening. IEEE Trans. Comput.-Aided Des. Integr. Circ. Syst. 39(7), 1524\u20131531 (2019)","DOI":"10.1109\/TCAD.2019.2915317"},{"issue":"2","key":"24_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. Form. Methods Syst. Des. 39(2), 205\u2013227 (2011)","journal-title":"Form. Methods Syst. Des."},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"Case, M.L., Mony, H., Baumgartner, J., Kanzelman, R:. Enhanced verification by temporal decomposition. In: 2009 Formal Methods in Computer-Aided Design, pp. 17\u201324. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351146"},{"key":"24_CR15","unstructured":"Cavada, R., et al.: The nuXmv symbolic model checker. In: Computer Aided Verification: 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, 18-22 July 2014. Proceedings 26, pp. 334\u2013342. Springer (2014)"},{"key":"24_CR16","unstructured":"Claessen, K., S\u00f6rensson, N.: A liveness checking algorithm that counts. In: 2012 Formal Methods in Computer-Aided Design (FMCAD), pp. 52\u201359. IEEE (2012)"},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"De Moura, L., Kong, S., Avigad, J., Van Doorn, F., von Raumer, J.: The Lean theorem prover (system description). In: Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, 1-7 August 2015, Proceedings 25, pp. 378\u2013388. Springer (2015)","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"24_CR18","unstructured":"The\u00a0LeanSAT Developers. LeanSAT"},{"key":"24_CR19","unstructured":"Dutertre, B., De\u00a0Moura, L.: The Yices SMT solver. 2(2), 1\u20132 (2006), Tool paper athttp:\/\/yices.csl.sri.com\/tool-paper.pdf"},{"key":"24_CR20","doi-asserted-by":"crossref","unstructured":"Froleyks, N., Yu, E., Biere, A., Heljanko, K.: Certifying phase abstraction. In: International Joint Conference on Automated Reasoning, pp. 284\u2013303. Springer (2024)","DOI":"10.1007\/978-3-031-63498-7_17"},{"key":"24_CR21","unstructured":"Gadgil, S., Rao, A.: Saturn: experiments with SAT solvers with proofs in Lean 4, 2025. Accessed 19 May 2025"},{"key":"24_CR22","doi-asserted-by":"crossref","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische schlie\u00dfen. i. Mathematische zeitschrift, vol. 35 (1935)","DOI":"10.1007\/BF01201353"},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"Griggio, A., Roveri, M., Tonetta, S.: Certifying proofs for LTL model checking. In: 2018 Formal Methods in Computer Aided Design (FMCAD), pp. 1\u20139. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8603022"},{"issue":"2","key":"24_CR24","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":"24_CR25","doi-asserted-by":"crossref","unstructured":"Mohamed, A.,et al.: Lean-SMT: an SMT tactic for discharging proof goals in Lean. In: Proceedings of the 37th International Conference on Computer Aided Verification (CAV 2025) (2025)","DOI":"10.1007\/978-3-031-98682-6_11"},{"key":"24_CR26","unstructured":"Munoz, C.A.: Batch proving and proof scripting in PVS. Technical report, National Institute of Aerospace (2007)"},{"key":"24_CR27","doi-asserted-by":"crossref","unstructured":"Namjoshi, K.S.: Certifying model checkers. In: Computer Aided Verification: 13th International Conference, CAV 2001 Paris, France, 18\u201322 July 2001 Proceedings 13, pp. 2\u201313. Springer (2001)","DOI":"10.1007\/3-540-44585-4_2"},{"key":"24_CR28","unstructured":"NASA. PVS-nasalib LTL library. https:\/\/github.com\/nasa\/pvslib\/tree\/master\/LTL. Accessed: 21 Feb 2025"},{"key":"24_CR29","doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: International Conference on Automated Deduction, pp. 748\u2013752. Springer (1992)","DOI":"10.1007\/3-540-55602-8_217"},{"key":"24_CR30","unstructured":"Owre, S., Shankar, N.: Writing PVS proof strategies. In: Design and Application of Strategies\/Tactics in Higher Order Logics (STRATA 2003), number CP-2003-212448 in NASA Conference Publication, pp. 1\u201315 (2003)"},{"key":"24_CR31","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"24_CR32","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Arons, T.: TLPVS: a PVS-based LTL verification system. In: Verification: Theory and Practice: Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday, pp. 598\u2013625. Springer (2003)","DOI":"10.1007\/978-3-540-39910-0_26"},{"key":"24_CR33","unstructured":"Rushby, J.: PVS embeddings of propositional and quantified modal logic. arXiv preprint arXiv:2205.06391 (2022)"},{"issue":"2","key":"24_CR34","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"C-JH Seger","year":"1995","unstructured":"Seger, C.-J.H., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Form. Methods Syst. Des. 6(2), 147\u2013189 (1995)","journal-title":"Form. Methods Syst. Des."},{"key":"24_CR35","unstructured":"Shankar, N., Owre, S., Rushby, J.M., Stringer-Calvert, D.W.: Stringer-Calvert. PVS prover guide. Computer Science Laboratory, SRI International, Menlo Park, CA, 1, 11\u201312 (2001)"},{"key":"24_CR36","unstructured":"Sindoni, G., et al.: Fbk-pdt-cert25. https:\/\/gitlab.fbk.eu\/gsindoni\/fbk_pdt_cert25. Accessed 24 02 2025"},{"key":"24_CR37","doi-asserted-by":"crossref","unstructured":"Yu, E., Biere, A., Heljanko, K.: Progress in certifying hardware model checking results. In: Computer Aided Verification: 33rd International Conference, CAV 2021, Virtual Event, 20\u201323 July 2021, Proceedings, Part II 33, pp. 363\u2013386. Springer (2021)","DOI":"10.1007\/978-3-030-81688-9_17"},{"key":"24_CR38","unstructured":"Yu, E., Froleyks, N., Biere, A., Heljanko, K.: Towards compositional hardware model checking certification. In: 2023 Formal Methods in Computer-Aided Design (FMCAD), pp. 1\u201311. IEEE (2023)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 30"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-99984-0_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T15:26:26Z","timestamp":1781882786000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-99984-0_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031999833","9783031999840"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-99984-0_24","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":"30 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 article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Discolusure of Interests"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Stuttgart","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","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":"28 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.dhbw-stuttgart.de\/cade-30\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}