通过计算范围缩减进行缺陷探测
计算机科学中的逻辑
2014-10-14 v4
摘要
我们描述了一种称为计算范围缩减（Computing Range Reduction, CRR）的模型检测方法。CRR 方法基于推导子句，以缩减可达状态轨迹集的方式，使得至少保留一个反例（如果存在）。这些子句是通过一种称为部分量词消去（Partial Quantifier Elimination, PQE）的技术推导出来的。给定一个数 n，CRR 方法可以找到长度小于或等于 n 的反例，或者证明此类反例不存在。我们通过实验表明，我们之前开发的 PQE 求解器可以有效地应用于推导现实基准测试中转换关系的约束子句。CRR 方法最吸引人的特点之一是它有可能找到长反例。这是它能够击败计算可达状态（或其近似值，如 IC3）的模型检测器或基于 SAT 的有界模型检测方法的领域。PQE 无法被 SAT 求解器有效模拟。这一点很重要，因为当前的模型检测研究主要由基于 SAT 的算法主导。CRR 方法提醒人们不应将所有鸡蛋放在一个篮子里。
引用
@article{arxiv.1408.7039,
title = {Bug Hunting By Computing Range Reduction},
author = {Eugene Goldberg and Panagiotis Manolios},
journal= {arXiv preprint arXiv:1408.7039},
year = {2014}
}
备注
The only difference of this version from the previous one is in Section 2. We added a comparison of the performance of the CRR method and other model checkers on an abstract counter