A theorem prover based approach for SAT-based model checking certification

DOI10.1007/978-3-031-99984-0_24MaRDI QIDQ6869936zbMATH OpenFDO

Authors Giulia Sindoni, P. Pasini, G. Cabodi, Paolo E. Camurati, Alberto Griggio, Marco Palena, Marco Roveri, Stefano Tonetta

Publication date 21 January 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-99984-0_24

zbMATH Keywords

certificateinvariantmodel checkingproof checkingsafety

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• \textsc{tlpvs}: A \textsc{pvs}-based \textsc{ltl} verification system
• An abstraction algorithm for the verification of level-sensitive latch-based netlists
• Benchmarking a model checker for algorithmic improvements and tuning for performance
• Certifying phase abstraction
• Certifying proofs for SAT-based model checking
• scientific article; zbMATH DE number 1798181 (Why is no real title available?)
• Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking
• Progress in certifying hardware model checking results
• SAT solver management strategies in IC3: an experimental approach
• The Lean theorem prover (system description)

This page was built for publication: A theorem prover based approach for SAT-based model checking certification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6869936)