论文标题
自动分离逻辑验证符（扩展版本）中的验证预言插入
Verification-Preserving Inlining in Automatic Separation Logic Verifiers (extended version)
论文作者
论文摘要
事实证明，有限验证对于检测错误并增加对程序正确性的信心很有用。与无限验证相反，通过（边界）内部和循环通过（有限的）展开的循环的推理不需要方法规格和循环不变式，因此，将开头的注释开销降低到裸露的最小值，即对要验证的属性的规格。对于基于传统程序逻辑的验证者，通过内部（和展开）保留验证：成功的无限验证W.R.T.一些注释意味着成功验证了内线程序。也就是说，在嵌入式程序中检测到的任何错误都会在原始程序中揭示出真正的错误。但是，这种基本属性可能无法适用于基于毒蛇的自动分离逻辑验证符，例如刺山柑，蚱hopper，grasshopper，炼油，钢，验证和验证仪。在这种情况下，内部通常会更改方法执行所拥有的资源，这可能会影响自动证明搜索算法并引入虚假错误。 在本文中，我们介绍了在自动分离逻辑验证符中验证验证核能内部的第一种技术。我们确定了有关程序的语义条件，并在Isabelle/HOL中证明它可以确保对最新的自动分离逻辑验证器的验证提供内衬。我们还证明了一个双重结果：成功验证嵌入式程序可确保有方法和循环注释可以验证有限执行的原始程序。为了自动检查我们的语义条件，我们提出了两个可以通过句法和程序验证者进行检查的近似值。我们在Viper中实施这些检查，并证明它们对于来自不同验证者的非平凡示例有效。
Bounded verification has proved useful to detect bugs and to increase confidence in the correctness of a program. In contrast to unbounded verification, reasoning about calls via (bounded) inlining and about loops via (bounded) unrolling does not require method specifications and loop invariants and, therefore, reduces the annotation overhead to the bare minimum, namely specifications of the properties to be verified. For verifiers based on traditional program logics, verification is preserved by inlining (and unrolling): successful unbounded verification of a program w.r.t. some annotation implies successful verification of the inlined program. That is, any error detected in the inlined program reveals a true error in the original program. However, this essential property might not hold for automatic separation logic verifiers such as Caper, GRASShopper, RefinedC, Steel, VeriFast, and verifiers based on Viper. In this setting, inlining generally changes the resources owned by method executions, which may affect automatic proof search algorithms and introduce spurious errors. In this paper, we present the first technique for verification-preserving inlining in automatic separation logic verifiers. We identify a semantic condition on programs and prove in Isabelle/HOL that it ensures verification-preserving inlining for state-of-the-art automatic separation logic verifiers. We also prove a dual result: successful verification of the inlined program ensures that there are method and loop annotations that enable the verification of the original program for bounded executions. To check our semantic condition automatically, we present two approximations that can be checked syntactically and with a program verifier, respectively. We implement these checks in Viper and demonstrate that they are effective for non-trivial examples from different verifiers.
