Book chapter
Towards Bit-Width-Independent Proofs in SMT Solvers
Automated Deduction – CADE 27, pp.366-384
Lecture Notes in Computer Science, Springer International Publishing
08/20/2019
DOI: 10.1007/978-3-030-29436-6_22
Abstract
Many SMT solvers implement efficient SAT-based procedures for solving fixed-size bit-vector formulas. These approaches, 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, this approach can still solve many formulas 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 rewrites.
Details
- Title: Subtitle
- Towards Bit-Width-Independent Proofs in SMT Solvers
- Creators
- Aina Niemetz - Stanford UniversityMathias Preiner - Stanford UniversityAndrew Reynolds - University of IowaYoni Zohar - Stanford UniversityClark Barrett - Stanford UniversityCesare Tinelli - University of Iowa
- Resource Type
- Book chapter
- Publication Details
- Automated Deduction – CADE 27, pp.366-384
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-030-29436-6_22
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Publisher
- Springer International Publishing; Cham
- Language
- English
- Date published
- 08/20/2019
- Academic Unit
- Computer Science
- Record Identifier
- 9984259466202771
Metrics
16 Record Views