Towards bit-width-independent proofs in SMT solvers
From MaRDI portal
Publication:2305428
DOI10.1007/978-3-030-29436-6_22OpenAlexW2969652480MaRDI QIDQ2305428
Mathias Preiner, Yoni Zohar, Aina Niemetz, Clark Barrett, Andrew Reynolds, Cesare Tinelli
Publication date: 10 March 2020
Full work available at URL: https://arxiv.org/abs/1905.10434
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (2)
On solving quantified bit-vector constraints using invertibility conditions ⋮ Towards satisfiability modulo parametric bit-vectors
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Complexity of fixed-size bit-vector logics
- Decision procedures. An algorithmic point of view
- Designing theory solvers with extensions
- Counterexample-guided quantifier instantiation for synthesis in SMT
- SMTCoq: a plug-in for integrating SMT solvers into Coq
- Syntax-guided rewrite rule enumeration for SMT solvers
- Unification with abstraction and theory instantiation in saturation-based reasoning
- Revisiting enumerative instantiation
- Extending Sledgehammer with SMT solvers
- AVATAR: The Architecture for First-Order Theorem Provers
- Efficient E-Matching for SMT Solvers
- Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
- Logics in Artificial Intelligence
- Solving quantified bit-vectors using invertibility conditions
This page was built for publication: Towards bit-width-independent proofs in SMT solvers
