Certifying proofs for SAT-based model checking
type: Item
instance of: scholarly article
title: Certifying proofs for SAT-based model checking
author: Alberto Griggio
author: Marco Roveri
author: Stefano Tonetta
published in: Formal Methods in System Design
publication date: 2021-12-08T00:00:00Z
Mathematics Subject Classification ID: 68-XX
zbMATH DE Number: 7440321
zbMATH Keywords: certifying model checking
zbMATH Keywords: linear-time temporal logic
zbMATH Keywords: LTL
zbMATH Keywords: invariant checking
zbMATH Keywords: liveness
zbMATH Keywords: deductive proofs
describes a project that uses: MiniSat
describes a project that uses: CAVA LTL Modelchecker
describes a project that uses: MathSAT5
describes a project that uses: TeMP
describes a project that uses: TRP++
describes a project that uses: nuXmv
describes a project that uses: AIGER
MaRDI profile type: Publication
full work available at URL: s10703-021-00369-1
OpenAlex ID: W3177059862
Wikidata QID: Q113902760
cites work: From Model Checking to a Temporal Proof for Partial Models
cites work: SAT-Based Model Checking without Unrolling
cites work: The MathSAT5 SMT Solver
cites work: An LTL Proof System for Runtime Verification
cites work: Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations
cites work: A Proof System for the Linear Time μ-Calculus
cites work: Theory and Applications of Satisfiability Testing
cites work: On model checking for the \(\mu\)-calculus and its fragments
cites work: Automated Reasoning
cites work: Hardware and software: verification and testing. 9th international Haifa verification conference, HVC 2013, Haifa, Israel, November 5--7, 2013. Proceedings
cites work: From complementation to certification
cites work: Q4553254
cites work: Q4474227
cites work: Q4531749
cites work: Q5559220
DOI: 10.1007/S10703-021-00369-1
description: scientific article; zbMATH DE number 7440321