Compressing BMC Encodings with QBF

DOI10.1016/j.entcs.2006.12.022zbMath1277.68136OpenAlexW2108530105MaRDI QIDQ2864383

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

encodingQBFSATbounded model checking

Mathematics Subject Classification ID

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

Related Items (9)

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

Uses Software

• MiniSat
• QuBE++
• NuSMV
• QUBE

Cites Work

• Relationships between nondeterministic and deterministic tape complexities
• Partial Implicit Unfolding in the Davis-Putnam Procedure for Quantified Boolean Formulae
• Theory and Applications of Satisfiability Testing
• Correct Hardware Design and Verification Methods
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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