Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors
Abstract elided by the publisher.
Related papers
- Solving Quantified Bit-Vectors Using Invertibility Conditions CAV 2018
- Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors CAV 2019
- BDD-Based Formula Approximations for Quantified Bit-Vector Satisfiability TACAS 2026
- CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver CAV 2021
- Syntax-Guided Quantifier Instantiation TACAS 2021
- Symbolic bounds analysis of pointers, array indices, and accessed memory regions PLDI 2000
- Symbolic bounds analysis of pointers, array indices, and accessed memory regions TOPLAS 2005
- Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic TACAS 2020