Journal article
Towards Satisfiability Modulo Parametric Bit-vectors
Journal of automated reasoning, Vol.65(7), pp.1001-1025
10/01/2021
DOI: 10.1007/s10817-021-09598-9
Abstract
Many SMT solvers implement efficient SAT-based procedures for solving fixed-size bit-vector formulas. These techniques, however, cannot be used directly to reason about bit-vectors of symbolic bit-width. To address this shortcoming, we propose a translation from bit-vector formulas with parametric bit-width to formulas in a logic supported by SMT solvers that includes non-linear integer arithmetic, uninterpreted functions, and universal quantification. While this logic is undecidable, our approach can still solve many formulas that arise in practice by capitalizing on advances in SMT solving for non-linear arithmetic and universally quantified formulas. We provide several case studies in which we have applied this approach with promising results, including the bit-width independent verification of invertibility conditions, compiler optimizations, and bit-vector rewrite rules.
Details
- Title: Subtitle
- Towards Satisfiability Modulo Parametric Bit-vectors
- Creators
- Aina Niemetz - Stanford UniversityMathias Preiner - Stanford UniversityAndrew Reynolds - University of IowaYoni Zohar - Stanford UniversityClark Barrett - Stanford UniversityCesare Tinelli - University of Iowa
- Resource Type
- Journal article
- Publication Details
- Journal of automated reasoning, Vol.65(7), pp.1001-1025
- Publisher
- Springer Nature
- DOI
- 10.1007/s10817-021-09598-9
- ISSN
- 0168-7433
- eISSN
- 1573-0670
- Number of pages
- 25
- Grant note
- N68335-17-C-0558 / ONR; Office of Naval Research 1656926 / NSF; National Science Foundation (NSF) Stanford Center for Blockchain Research N66001-18-C-4012; FA8650-18-2-7861 / DARPA; United States Department of Defense; Defense Advanced Research Projects Agency (DARPA)
- Language
- English
- Date published
- 10/01/2021
- Academic Unit
- Computer Science
- Record Identifier
- 9984259464802771
Metrics
10 Record Views