“Towards
Bit-Width-Independent Proofs in SMT Solvers”
by Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark Barrett, and Cesare Tinelli.
In *Proceedings of the 27^th International Conference on
Automated Deduction (CADE '19)*, (Pascal Fontaine, ed.), Aug. 2019,
pp. 366-384. Natal, Brazil.

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.

**BibTeX entry:**

@inproceedings{NPR+19, author = {Aina Niemetz and Mathias Preiner and Andrew Reynolds and Yoni Zohar and Clark Barrett and Cesare Tinelli}, editor = {Pascal Fontaine}, title = {Towards Bit-Width-Independent Proofs in SMT Solvers}, booktitle = {Proceedings of the {\it 27^{th}} International Conference on Automated Deduction (CADE '19)}, series = {Lecture Notes in Artificial Intelligence}, volume = {11716}, pages = {366--384}, publisher = {Springer}, month = aug, year = {2019}, note = {Natal, Brazil}, url = {http://theory.stanford.edu/~barrett/pubs/NPR+19.pdf} }

(This webpage was created with bibtex2web.)