公式切片：来自前提的归纳不变量
Formula Slicing: Inductive Invariants from Preconditions
摘要：
我们提出了一个“公式切片”的方法来寻找归纳不变量。它基于这样的观察：程序中的许多循环只影响内存的一小部分，并且许多在循环之前有效的不变量在循环之后仍然有效。给定一个循环的前提条件，从前面的程序片段中获得，我们削弱它，直到它成为归纳的。弱化过程由SMT求解器给出的归纳法的反例指导。我们的算法适用于任意循环结构的程序，它计算的最强不变量在一个抽象域的削弱的先决条件。我们称这个算法为“公式切片”，因为它有效地执行“切片”公式从符号执行。我们评估我们的算法的设备驱动程序的基准测试从国际软件验证比赛（SV-COMP），我们表明，它是具有竞争力的国家的最先进的验证技术。
英文摘要：
We propose a "formula slicing" method for finding inductive invariants. It is based on the observation that many loops in the program affect only a small part of the memory, and many invariants which were valid before a loop are still valid after. Given a precondition of the loop, obtained from the preceding program fragment, we weaken it until it becomes inductive. The weakening procedure is guided by counterexamples-to-induction given by an SMT solver. Our algorithm applies to programs with arbitrary loop structure, and it computes the strongest invariant in an abstract domain of weakenings of preconditions. We call this algorithm "formula slicing", as it effectively performs "slicing" on formulas derived from symbolic execution. We evaluate our algorithm on the device driver benchmarks from the International Competition on Software Verification (SV-COMP), and we show that it is competitive with the state-of-the-art verification techniques.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
