Bounded model checking with QBF

DOI10.1007/11499107_32MaRDI QIDQ5713732zbMATH OpenOpenAlexFDO

Authors Nachum Dershowitz, Ziyad Hanna, Jacob Katz

Publication date 15 December 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b137280

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Bounded model checking using satisfiability solving
• Semi-formal bounded model checking
• Bounded Model Checking with Description Logic Reasoning
• Model Checking Quantified Computation Tree Logic
• Bounded LTL model checking with stable models
• \(\mathsf{QCTL}\) model-checking with \(\mathsf{QBF}\) solvers
• Bounded ITL model checking with stable models
• Bounded Model Checking for Partial Kripke Structures
• Lattice-based refinement in bounded model checking

Cited in

(27)

• A self-adaptive multi-engine solver for quantified Boolean formulas
• Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
• Unified QBF certification and its applications
• Bounded model checking with SNF, alternating automata, and Büchi automata
• Bounded model checking with parametric data structures
• Compressing BMC encodings with QBF
• Abstraction-based algorithm for 2QBF
• Transformations into normal forms for quantified circuits
• Validating QBF Validity in HOL4
• Proving Valid Quantified Boolean Formulas in HOL Light
• QELL: QBF reasoning with extended clause learning and levelized SAT solving
• Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
• A Compact Representation for Syntactic Dependencies in QBFs
• A fixpoint based encoding for bounded model checking
• Verification of partial designs using incremental QBF
• Efficient reduction of nondeterministic automata with application to language inclusion testing
• scientific article; zbMATH DE number 7029312 (Why is no real title available?)
• Semi-formal bounded model checking
• Size, cost and capacity: a semantic technique for hard random QBFs
• Efficiently representing existential dependency sets for expansion-based QBF solvers
• Encoding Queues in Satisfiability Modulo Theories Based Bounded Model Checking
• Analysis of search based algorithms for satisfiability of propositional and quantified Boolean formulas arising from circuit state space diameter problems
• Model checking quantitative hyperproperties
• Gray-box runtime enforcement of hyperproperties
• \(\mathsf{QCTL}\) model-checking with \(\mathsf{QBF}\) solvers
• Deciding effectively propositional logic using DPLL and substitution sets
• CSL model checking algorithms for QBDs

This page was built for publication: Bounded model checking with QBF

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