“Towards Satisfiability Modulo Parametric Bit-vectors” by Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark Barrett, and Cesare Tinelli. Journal of Automated Reasoning, vol. 65, no. 7, Oct. 2021, pp. 1001-1025, Springer.
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.
Keywords: Satisfiability Modulo Theories, Bit-precise Reasoning, Parametric Bit-vectors
BibTeX entry:
@article{NPR+21c,
author = {Aina Niemetz and Mathias Preiner and Andrew Reynolds and Yoni
Zohar and Clark Barrett and Cesare Tinelli},
title = {Towards Satisfiability Modulo Parametric Bit-vectors},
journal = {Journal of Automated Reasoning},
volume = {65},
number = {7},
pages = {1001--1025},
publisher = {Springer},
month = oct,
year = {2021},
doi = {10.1007/s10817-021-09598-9},
url = {http://theory.stanford.edu/~barrett/pubs/NPR+21c.pdf}
}
(This webpage was created with bibtex2web.)