On solving quantified bit-vector constraints using invertibility conditions

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

zbMATH Keywords

invertibility conditionssatisfiability modulo theoriesquantified bit-vectors

Mathematics Subject Classification ID

Computer science (68-XX)

Related Items

Synthesising programs with non-trivial constants ⋮ Syntax-guided quantifier instantiation ⋮ Towards satisfiability modulo parametric bit-vectors

Uses Software

• Coq
• Yices
• z3
• StarExec
• CVC4
• SMTCoq
• CVC4SY

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