“Solving Quantified Bit-Vectors using Invertibility Conditions” by Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. In Proceedings of the 30^th International Conference on Computer Aided Verification (CAV '18), (Hana Chockler and Georg Weissenbacher, eds.), July 2018, pp. 236-255. Oxford, United Kingdom.
We present a novel approach for solving quantified bit-vector formulas in Satisfiability Modulo Theories (SMT) based on computing symbolic inverses of bit-vector operators. We derive conditions that precisely characterize when bit-vector constraints are invertible for a representative set of bit-vector operators commonly supported by SMT solvers. We utilize syntax-guided synthesis techniques to aid in establishing these conditions and verify them independently by using several SMT solvers. We show that invertibility conditions can be embedded into quantifier instantiations using Hilbert choice expressions, and give experimental evidence that a counterexample-guided approach for quantifier instantiation utilizing these techniques leads to performance improvements with respect to state-of-the-art solvers for quantified bit-vector constraints.
BibTeX entry:
@inproceedings{NPR+18,
author = {Aina Niemetz and Mathias Preiner and Andrew Reynolds and
Clark Barrett and Cesare Tinelli},
editor = {Hana Chockler and Georg Weissenbacher},
title = {Solving Quantified Bit-Vectors using Invertibility Conditions},
booktitle = {Proceedings of the {\it 30^{th}} International Conference
on Computer Aided Verification (CAV '18)},
series = {Lecture Notes in Computer Science},
volume = {10982},
pages = {236--255},
publisher = {Springer},
month = jul,
year = {2018},
isbn = {978-3-319-96142-2},
doi = {10.1007/978-3-319-96142-2_16},
note = {Oxford, United Kingdom},
url = {http://theory.stanford.edu/~barrett/pubs/NPR+18.pdf}
}
(This webpage was created with bibtex2web.)