内插强归纳法
Interpolating Strong Induction
摘要：
强归纳原理，也被称为k-归纳，是基于无界SAT的模型检验（SMC）的第一批技术之一。虽然优雅和简单的应用，这样的属性很少是k-归纳的，当它们可以加强时，没有有效的策略来猜测归纳的深度。它主要被基于插值和属性定向可达性（Pdr）计算感应增强的技术所取代。在本文中，我们提出了kAvy，SMC算法，有效地使用k-归纳指导插值和Pdr风格的归纳推广。与纯k-归纳不同，kAvy使用Pdr风格的推广来计算和加强归纳迹。与纯Pdr不同，kAvy使用相对k-归纳来构造归纳不变量。通过最小化不可满足性的证明来动态地调整归纳的深度。我们已经在Avy Model中实现了kAvy，并在HWMCC实例上对其进行了评估。我们的研究结果表明，kAvy比Avy和Pdr更有效，并且使用k-归纳会导致更快的运行时间和解决更多的实例。此外，在一类称为shift的基准测试中，kAvy比Avy、Pdr和k-归纳快几个数量级。
英文摘要：
The principle of strong induction, also known as k-induction is one of the first techniques for unbounded SAT-based Model Checking (SMC). While elegant and simple to apply, properties as such are rarely k-inductive and when they can be strengthened, there is no effective strategy to guess the depth of induction. It has been mostly displaced by techniques that compute inductive strengthenings based on interpolation and property directed reachability (Pdr). In this paper, we present kAvy, an SMC algorithm that effectively uses k-induction to guide interpolation and Pdr-style inductive generalization. Unlike pure k-induction, kAvy uses Pdr-style generalization to compute and strengthen an inductive trace. Unlike pure Pdr, kAvy uses relative k-induction to construct an inductive invariant. The depth of induction is adjusted dynamically by minimizing a proof of unsatisfiability. We have implemented kAvy within the Avy Model Checker and evaluated it on HWMCC instances. Our results show that kAvy is more effective than both Avy and Pdr, and that using k-induction leads to faster running time and solving more instances. Further, on a class of benchmarks, called shift, kAvy is orders of magnitude faster than Avy, Pdr and k-induction.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
