Compressing BMC encodings with QBF

DOI10.1016/J.ENTCS.2006.12.022MaRDI QIDQ2864383zbMATH OpenOpenAlexFDO

Authors Toni Jussila, Armin Biere

Publication date 6 December 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2006.12.022

zbMATH Keywords

bounded model checkingencodingQBFSAT

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Theory and Applications of Satisfiability Testing
• scientific article; zbMATH DE number 2084774
• QBF Encoding of Temporal Properties and QBF-Based Verification
• Principles and Practice of Constraint Programming – CP 2004
• scientific article; zbMATH DE number 5542982

Cites work

• Correct Hardware Design and Verification Methods
• scientific article; zbMATH DE number 3560737 (Why is no real title available?)
• scientific article; zbMATH DE number 1953038 (Why is no real title available?)
• scientific article; zbMATH DE number 1765680 (Why is no real title available?)
• scientific article; zbMATH DE number 1903365 (Why is no real title available?)
• scientific article; zbMATH DE number 2102695 (Why is no real title available?)
• scientific article; zbMATH DE number 3313427 (Why is no real title available?)
• Partial implicit unfolding in the Davis-Putnam procedure for quantified Boolean formulae
• Relationships between nondeterministic and deterministic tape complexities
• Report of the third QBF solvers evaluation
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing

Cited in

(9)

• A self-adaptive multi-engine solver for quantified Boolean formulas
• A formal methods approach to predicting new features of the eukaryotic vesicle traffic system
• Ranking function synthesis for bit-vector relations
• Linear templates of ACTL formulas with an application to SAT-based verification
• The QBF Gallery: behind the scenes
• Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
• A Compact Representation for Syntactic Dependencies in QBFs
• Efficiently representing existential dependency sets for expansion-based QBF solvers
• Formal methods for NFA equivalence: QBFs, witness extraction, and encoding verification

Describes a project that uses

Uses Software

• MiniSat
• NuSMV
• QuBE++
• QUBE

This page was built for publication: Compressing BMC encodings with QBF

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