一种用于求解位向量上困难 SMT 实例的增量抽象方案
计算机科学中的逻辑
2020-08-25 v1
摘要
基于位向量理论的 SMT 问题判定过程是当前软硬件验证器中的基本组件。尽管总体上非常高效，某些 SMT 实例对现有求解器仍具挑战性（尤其当此类实例包含计算代价高昂的函数时）。本文中，我们提出一种基于增量 SMT 求解与抽象精化的无量词位向量理论（SMT-LIB 中的 QF_BV）方法。我们针对乘法、除法与取余算子定义了四种具体近似步骤，并将其组合为一个增量抽象方案。我们在扩展 SMT 求解器 Boolector 的原型中实现了该方案，并测量了整体性能及单步近似的性能。评估表明，我们的抽象方案有助于求解更多不可满足的基准实例，包括 SMT-LIB 中七个状态未知的实例。
引用
@article{arxiv.2008.10061,
title = {An Incremental Abstraction Scheme for Solving Hard SMT-Instances over Bit-Vectors},
author = {Samuel Teuber and Marko Kleine Büning and Carsten Sinz},
journal= {arXiv preprint arXiv:2008.10061},
year = {2020}
}