Towards Bit-Width-Independent Proofs in SMT Solvers

“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.

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.

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.)