Efficiently solving quantified bit-vector formulas
From MaRDI portal
Recommendations
- Solving quantified bit-vector formulas using binary decision diagrams
- Solving quantified bit-vectors using invertibility conditions
- On solving quantified bit-vector constraints using invertibility conditions
- A bit-vector solver with word-level propagation
- Matching multiplications in bit-vector formulas
Cites work
- scientific article; zbMATH DE number 5613976 (Why is no real title available?)
- scientific article; zbMATH DE number 5539366 (Why is no real title available?)
- scientific article; zbMATH DE number 4124989 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- A Decision Procedure for Bit-Vectors and Arrays
- A solver for QBFs in negation normal form
- An abstract decision procedure for satisfiability in the theory of recursive data types
- Beyond CNF: A Circuit-Based QBF Solver
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Complexity results for classes of quantificational formulas
- Constraint-Based Invariant Inference over Predicate Abstraction
- Efficient E-Matching for SMT Solvers
- Fault Localization and Correction with QBF
- Formal Methods in Computer-Aided Design
- From program verification to program synthesis
- Integrating dependency schemes in search-based QBF solvers
- Logic for Programming, Artificial Intelligence, and Reasoning
- Ranking function synthesis for bit-vector relations
- Schema-Guided Synthesis of Imperative Programs by Constraint Solving
- Theory and Applications of Satisfiability Testing
- Verification, Model Checking, and Abstract Interpretation
Cited in
(32)- Solving QBF with counterexample guided refinement
- On the complexity of the quantified bit-vector arithmetic with binary encoding
- More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding
- A bit-vector solver with word-level propagation
- Synthesis of domain specific CNF encoders for bit-vector solvers
- Syntax-guided quantifier instantiation
- On solving quantified bit-vector constraints using invertibility conditions
- Array theory of bounded elements and its applications
- Matching multiplications in bit-vector formulas
- Truncating abstraction of bit-vector operations for BDD-based SMT solvers
- Synthesis for Unbounded Bit-Vector Arithmetic
- Abstraction-based algorithm for 2QBF
- Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors
- Solving quantified bit-vectors using invertibility conditions
- Bit-vector algorithms for binary constraint satisfaction and subgraph isomorphism
- Refutation-based synthesis in SMT
- Fast three-valued abstract bit-vector arithmetic
- Deciding Bit-Vector Formulas with mcSAT
- Synchronous counting and computational algorithm design
- Solving quantified bit-vector formulas using binary decision diagrams
- Incremental determinization
- Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
- Ranking function synthesis for bit-vector relations
- Functional analysis of large-scale DNA strand displacement circuits
- A layered algorithm for quantifier elimination from linear modular constraints
- Proving LTL Properties of Bitvector Programs and Decompiled Binaries
- On Incremental Pre-processing for SMT
- Solving quantified linear arithmetic by counterexample-guided instantiation
- Complexity of fixed-size bit-vector logics
- Sharpening constraint programming approaches for bit-vector theory
- Counterexample-Guided Model Synthesis
- bv2epr: a tool for polynomially translating quantifier-free bit-vector formulas into EPR
Describes a project that uses
Uses Software
This page was built for publication: Efficiently solving quantified bit-vector formulas
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2441770)
