On solving quantified bit-vector constraints using invertibility conditions

DOI10.1007/S10703-020-00359-9MaRDI QIDQ2050109zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

satisfiability modulo theoriesinvertibility conditionsquantified bit-vectors

Mathematics Subject Classification ID

Computer science (68-XX)

Recommendations

• Solving quantified bit-vectors using invertibility conditions
• Counterexample-Guided Model Synthesis
• Solving quantified bit-vector formulas using binary decision diagrams
• Efficiently solving quantified bit-vector formulas
• Syntax-guided quantifier instantiation

Cites work

• scientific article; zbMATH DE number 3408928 (Why is no real title available?)
• A layered algorithm for quantifier elimination from linear modular constraints
• A mathematical introduction to logic.
• Applying Linear Quantifier Elimination
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Counterexample-Guided Model Synthesis
• Counterexample-guided quantifier instantiation for synthesis in SMT
• Efficiently solving quantified bit-vector formulas
• Precise and complete propagation based local search for satisfiability modulo theories
• Proceedings Sixth Workshop on Proof eXchange for Theorem Proving
• Propagation based local search for bit-precise reasoning
• SMTCoq: a plug-in for integrating SMT solvers into Coq
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Solving quantified bit-vector formulas using binary decision diagrams
• Solving quantified bit-vectors using invertibility conditions
• Solving quantified linear arithmetic by counterexample-guided instantiation
• Towards bit-width-independent proofs in SMT solvers

Cited in

(14)

• 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
• Invertibility conditions for floating-point formulas
• Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors
• Solving quantified bit-vectors using invertibility conditions
• 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
• Formal Verification of Bit-Vector Invertibility Conditions in Coq
• Sharpening constraint programming approaches for bit-vector theory
• \textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format

Describes a project that uses

Uses Software

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

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)