On solving quantified bit-vector constraints using invertibility conditions
From MaRDI portal
Publication:2050109
DOI10.1007/S10703-020-00359-9OpenAlexW3124136127MaRDI QIDQ2050109FDOQ2050109
Authors: Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli 
Publication date: 30 August 2021
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1804.05025
Recommendations
Cites Work
- Efficiently solving quantified bit-vector formulas
- A mathematical introduction to logic.
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Applying Linear Quantifier Elimination
- Title not available (Why is that?)
- Counterexample-guided quantifier instantiation for synthesis in SMT
- SMTCoq: a plug-in for integrating SMT solvers into Coq
- Proceedings Sixth Workshop on Proof eXchange for Theorem Proving
- Solving quantified linear arithmetic by counterexample-guided instantiation
- Propagation based local search for bit-precise reasoning
- Precise and complete propagation based local search for satisfiability modulo theories
- Towards bit-width-independent proofs in SMT solvers
- A layered algorithm for quantifier elimination from linear modular constraints
- Solving quantified bit-vector formulas using binary decision diagrams
- Counterexample-Guided Model Synthesis
- Solving quantified bit-vectors using invertibility conditions
Cited In (12)
- Synthesising programs with non-trivial constants
- Synthesis of domain specific CNF encoders for bit-vector solvers
- Syntax-guided quantifier instantiation
- Towards satisfiability modulo parametric bit-vectors
- Solving quantified bit-vectors using invertibility conditions
- Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors
- Efficiently solving quantified bit-vector formulas
- A Bit-Scaling Algorithm for Integer Feasibility in UTVPI Constraints
- Solving quantified bit-vector formulas using binary decision diagrams
- Constraint satisfaction through GBP-guided deliberate bit flipping
- Sharpening constraint programming approaches for bit-vector theory
- \textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format
Uses Software
This page was built for publication: On solving quantified bit-vector constraints using invertibility conditions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2050109)
