zbMATH — the first resource for mathematics

Towards bit-width-independent proofs in SMT solvers. (English) Zbl 07178987
Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 366-384 (2019).
Summary: 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.
For the entire collection see [Zbl 1428.68018].

03B35 Mechanization of proofs and logical operations
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Full Text: DOI