Efficiently solving quantified bit-vector formulas
From MaRDI portal
Publication:2441770
DOI10.1007/s10703-012-0156-2zbMath1284.03212MaRDI QIDQ2441770
Leonardo de Moura, Christoph M. Wintersteiger, Youssef Hamadi
Publication date: 28 March 2014
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10703-012-0156-2
03B70: Logic in computer science
68Q60: Specification and verification (program logics, model checking, etc.)
68T20: Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Related Items
Functional Analysis of Large-Scale DNA Strand Displacement Circuits, Solving QBF with counterexample guided refinement, Complexity of fixed-size bit-vector logics, Synchronous counting and computational algorithm design, Solving quantified linear arithmetic by counterexample-guided instantiation, On the complexity of the quantified bit-vector arithmetic with binary encoding, On solving quantified bit-vector constraints using invertibility conditions, Syntax-guided quantifier instantiation, Ranking function synthesis for bit-vector relations, Refutation-based synthesis in SMT, Array theory of bounded elements and its applications, A layered algorithm for quantifier elimination from linear modular constraints, Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams, Incremental Determinization, Abstraction-Based Algorithm for 2QBF, Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL, Counterexample-Guided Model Synthesis
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A solver for QBFs in negation normal form
- Complexity results for classes of quantificational formulas
- An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types
- Ranking Function Synthesis for Bit-Vector Relations
- Constraint-Based Invariant Inference over Predicate Abstraction
- Efficient E-Matching for SMT Solvers
- Fault Localization and Correction with QBF
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Beyond CNF: A Circuit-Based QBF Solver
- Integrating Dependency Schemes in Search-Based QBF Solvers
- From program verification to program synthesis
- A Decision Procedure for Bit-Vectors and Arrays
- Schema-Guided Synthesis of Imperative Programs by Constraint Solving
- Formal Methods in Computer-Aided Design
- Logic for Programming, Artificial Intelligence, and Reasoning
- Theory and Applications of Satisfiability Testing
- Verification, Model Checking, and Abstract Interpretation
