Finding bugs efficiently with a SAT solver
Finding bugs efficiently with a SAT solver
复制标题
使用 SAT 求解器有效查找错误
DOI：
10.1145/1287624.1287653
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
F. Tip
中科院分区：
文献类型：
--
作者：
Julian T Dolby;M. Vaziri;F. Tip
我们提出了一种方法来检查代码对丰富的规范，现有的工作，包括编码的程序在关系逻辑和使用约束求解器，以找到规范违反的基础上。我们提高了这种方法的效率与一个新的编码的程序，有效地切片它在逻辑层面上的规范。我们还提出了新的整数值和数组的编码，使现实的代码片段，操纵两者的验证。我们的技术可以处理比以前可能的范围更大的整数，并允许大型稀疏数组被有效地处理。
我们提出了一个合理的证明，我们的切片算法和关系公式可以切片的一般条件。我们实现了我们的技术，并通过检查从Java集合框架中提取的几个类的数据结构不变量对其进行评估。我们还检查了各种开源程序中违反Java平等契约的情况，并发现了几个bug。
We present an approach for checking code against rich specifications, based on existing work that consists of encoding the program in a relational logic and using a constraint solver to find specification violations. We improve the efficiency of this approach with a new encoding of the program that effectively slices it at the logical level with respect to the specification. We also present new encodings for integer values and arrays, enabling the verification of realistic fragments of code that manipulate both. Our technique can handle integers of much larger ranges than previously possible, and permits large sparse arrays to be handled efficiently.
We present a soundness proof for our slicing algorithm and a general condition under which relational formulae may be sliced. We implemented our technique and evaluated it by checking data structure invariants of several classes taken from the Java Collections Framework. We also checked for violations of Java's equality contract in a variety of open-source programs, and found several bugs.