Certifying proofs for SAT-based model checking

DOI10.1007/s10703-021-00369-1OpenAlexW3177059862WikidataQ113902760 ScholiaQ113902760MaRDI QIDQ2058379

Stefano Tonetta, Marco Roveri, Alberto Griggio

Publication date: 8 December 2021

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-021-00369-1

zbMATH Keywords

livenessLTLlinear-time temporal logiccertifying model checkingdeductive proofsinvariant checking

Mathematics Subject Classification ID

Computer science (68-XX)

Related Items (5)

Automated Verification of Parallel Nested DFS ⋮ Verified Certification of Reachability Checking for Timed Automata ⋮ Integrating Topological Proofs with Model Checking to Instrument Iterative Design ⋮ Progress in certifying hardware model checking results ⋮ TOrPEDO : witnessing model correctness with topological proofs

Uses Software

• MiniSat
• MathSAT5
• TeMP
• TRP++
• nuXmv
• CAVA LTL Modelchecker
• AIGER

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Hardware and software: verification and testing. 9th international Haifa verification conference, HVC 2013, Haifa, Israel, November 5--7, 2013. Proceedings
• From complementation to certification
• SAT-Based Model Checking without Unrolling
• Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations
• From Model Checking to a Temporal Proof for Partial Models
• An LTL Proof System for Runtime Verification
• Automated Reasoning
• Theory and Applications of Satisfiability Testing
• The MathSAT5 SMT Solver
• A Proof System for the Linear Time μ-Calculus
• On model checking for the \(\mu\)-calculus and its fragments

This page was built for publication: Certifying proofs for SAT-based model checking