论文标题
一个增量抽象方案，用于在位矢量上求解硬smt的现场
An Incremental Abstraction Scheme for Solving Hard SMT-Instances over Bit-Vectors
论文作者
论文摘要
基于位矢量理论的SMT问题的决策程序是最先进的软件和硬件验证器中的基本组成部分。尽管通常非常有效，但某些SMT实例仍然对最先进的求解器仍然具有挑战性（尤其是当这些实例包含计算昂贵的功能时）。在这项工作中，我们提出了一种基于增量SMT求解和抽象细化的无量词比特矢量理论（SMT-LIB中的QF_BV）的方法。我们为乘法，除法和剩余操作员定义了四个混凝土近似步骤，并将它们合并为增量抽象方案。我们在扩展SMT求解器布洛尔仪的原型中实现此方案，并测量单个近似步骤的整体性能和性能。评估表明，我们的抽象方案有助于解决更难以满足的基准实例，包括七个在SMT-LIB中状态未知的实例。
Decision procedures for SMT problems based on the theory of bit-vectors are a fundamental component in state-of-the-art software and hardware verifiers. While very efficient in general, certain SMT instances are still challenging for state-of-the-art solvers (especially when such instances include computationally costly functions). In this work, we present an approach for the quantifier-free bit-vector theory (QF_BV in SMT-LIB) based on incremental SMT solving and abstraction refinement. We define four concrete approximation steps for the multiplication, division and remainder operators and combine them into an incremental abstraction scheme. We implement this scheme in a prototype extending the SMT solver Boolector and measure both the overall performance and the performance of the single approximation steps. The evaluation shows that our abstraction scheme contributes to solving more unsatisfiable benchmark instances, including seven instances with unknown status in SMT-LIB.
