On solving quantified bit-vector constraints using invertibility conditions
From MaRDI portal
Publication:2050109
DOI10.1007/S10703-020-00359-9OpenAlexW3124136127MaRDI QIDQ2050109FDOQ2050109
Aina Niemetz, Clark Barrett, Cesare Tinelli, Andrew Reynolds, Mathias Preiner
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
- 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 (9)
- Synthesising programs with non-trivial constants
- 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
- A Bit-Scaling Algorithm for Integer Feasibility in UTVPI Constraints
- 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)
