Towards Bit-Width-Independent Proofs in SMT Solvers
Towards Bit-Width-Independent Proofs in SMT Solvers
复制标题
在 SMT 求解器中实现与位宽无关的证明
DOI：
10.1007/978-3-030-29436-6_22
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
C. Tinelli
中科院分区：
文献类型：
--
作者：
Aina Niemetz;Mathias Preiner;Andrew Reynolds;Yoni Zohar;Clark W. Barrett;C. Tinelli
许多 SMT 求解器实现高效的基于 SAT 的过程来求解固定大小的位向量公式。然而，这些方法不能直接用于推理符号位宽度的位向量。为了解决这个缺点，我们提出了从非固定位宽的位向量公式到 SMT 求解器支持的逻辑公式的转换，其中包括非线性整数算术、未解释的函数和通用量化。虽然这种逻辑是不可判定的，但这种方法仍然可以通过利用 SMT 求解非线性算术和通用量化公式的进步来求解许多公式。我们提供了几个案例研究，其中我们应用了这种方法并取得了有希望的结果，包括可逆条件的位宽独立验证、编译器优化和位向量重写。
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 of non-fixed 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 advancements 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.
使用 SMT 求解器扩展 Sledgehammer
DOI：
10.1007/s10817-013-9278-5
发表时间：
2013
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
Jasmin Christian Blanchette;Sascha Böhme;Lawrence C. Paulson
通讯作者：
Lawrence C. Paulson