On solving quantified bit-vector constraints using invertibility conditions
From MaRDI portal
Publication:2050109
DOI10.1007/s10703-020-00359-9OpenAlexW3124136127MaRDI QIDQ2050109
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
Related Items
Synthesising programs with non-trivial constants ⋮ Syntax-guided quantifier instantiation ⋮ Towards satisfiability modulo parametric bit-vectors
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Solving quantified linear arithmetic by counterexample-guided instantiation
- Propagation based local search for bit-precise reasoning
- Counterexample-guided quantifier instantiation for synthesis in SMT
- SMTCoq: a plug-in for integrating SMT solvers into Coq
- Towards bit-width-independent proofs in SMT solvers
- A layered algorithm for quantifier elimination from linear modular constraints
- Efficiently solving quantified bit-vector formulas
- Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams
- Applying Linear Quantifier Elimination
- Counterexample-Guided Model Synthesis
- Solving SAT and SAT Modulo Theories
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories
- Proceedings Sixth Workshop on Proof eXchange for Theorem Proving
- Solving quantified bit-vectors using invertibility conditions
