“Bit-Precise Reasoning with Parametric Bit-Vectors” by Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. In Proceedings of the 28^th International Conference on Theory and Applications of Satisfiability Testing (SAT '25), (Jeremias Berg and Jakob Nordström, eds.), Aug. 2025, pp. 4:1-4:24. Glasgow, Scotland.
The SMT-LIB theory of bit-vectors is restricted to bit-vectors of fixed width. However, several important applications can benefit from reasoning about bit-vectors of symbolic widths, i.e., parametric bit-vectors. Recent work has introduced an approach for solving formulas over parametric bit-vectors, via an eager translation to quantified integer arithmetic with uninterpreted functions. The approach was shown to be successful for several applications, including the bit-width independent verification of compiler optimizations, invertibility conditions, and rewrite rules. We extend and improve that approach in several aspects. Theoretically, we improve expressiveness by defining a new theory of parametric bit-vectors that supports more operators and allows reasoning about the bit-widths themselves. Algorithmically, we introduce a lazy algorithm that avoids the use of uninterpreted functions and quantified axioms for them. Empirically, we show a significant improvement by implementing and evaluating our approach, and comparing it experimentally to the previous one.
BibTeX entry:
@inproceedings{BZN+25,
author = {Zvika Berger and Yoni Zohar and Aina Niemetz and Mathias
Preiner and Andrew Reynolds and Clark Barrett and Cesare Tinelli},
editor = {Jeremias Berg and Jakob Nordstr{\"o}m},
title = {Bit-Precise Reasoning with Parametric Bit-Vectors},
booktitle = {Proceedings of the {\it 28^{th}} International Conference
on Theory and Applications of Satisfiability Testing (SAT '25)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {341},
pages = {4:1--4:24},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
month = aug,
year = {2025},
doi = {10.4230/LIPIcs.SAT.2025.4},
note = {Glasgow, Scotland},
url =
{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.4}
}
(This webpage was created with bibtex2web.)