Journal article
On solving quantified bit-vector constraints using invertibility conditions
Formal methods in system design, Vol.57(1), pp.87-115
07/01/2021
DOI: 10.1007/s10703-020-00359-9
Abstract
We present a novel approach for solving quantified bit-vector constraints 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.
Details
- Title: Subtitle
- On solving quantified bit-vector constraints using invertibility conditions
- Creators
- Aina Niemetz - Stanford UniversityMathias Preiner - Stanford UniversityAndrew Reynolds - University of IowaClark Barrett - Stanford UniversityCesare Tinelli - University of Iowa
- Resource Type
- Journal article
- Publication Details
- Formal methods in system design, Vol.57(1), pp.87-115
- Publisher
- Springer Nature
- DOI
- 10.1007/s10703-020-00359-9
- ISSN
- 0925-9856
- eISSN
- 1572-8102
- Number of pages
- 29
- Grant note
- 1656926 / National Science Foundation; National Science Foundation (NSF) FA8750-15-C-0113; FA8650-18-2-7861 / DARPA; United States Department of Defense; Defense Advanced Research Projects Agency (DARPA)
- Language
- English
- Date published
- 07/01/2021
- Academic Unit
- Computer Science
- Record Identifier
- 9984259494002771
Metrics
8 Record Views