用于快速缺陷检测的反例引导k-归纳验证
Counterexample-Guided k-Induction Verification for Fast Bug Detection
摘要：
最近，k-induction算法已被证明是一个成功的方法，发现错误和证明正确性。然而，由于该算法是一个增量的方法，它可能会浪费资源试图证明不正确的程序。在本文中，我们提出了扩展的k-归纳算法，以缩短所需的步骤数，找到一个属性违反。我们将该算法转换成一个满足在中间的双向搜索算法，使用反例产生的过度近似的程序。初步结果表明，发现一个属性违反所需的步骤的数量减少到$\lfloor\frac{k}{2} + 1\rfloor$和验证时间的程序与大的状态空间大大减少。
英文摘要：
Recently, the k-induction algorithm has proven to be a successful approach for both finding bugs and proving correctness. However, since the algorithm is an incremental approach, it might waste resources trying to prove incorrect programs. In this paper, we propose to extend the k-induction algorithm in order to shorten the number of steps required to find a property violation. We convert the algorithm into a meet-in-the-middle bidirectional search algorithm, using the counterexample produced from over-approximating the program. The preliminary results show that the number of steps required to find a property violation is reduced to $\lfloor\frac{k}{2} + 1\rfloor$ and the verification time for programs with large state space is reduced considerably.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
