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.

翻译：有界验证已被证明在检测错误及增强程序正确性信心方面具有实用价值。与无界验证相比，通过（有界）内联处理调用及（有界）展开处理循环无需方法规约和循环不变量，从而将注释负担降至最低——仅需针对待验证属性进行规约。对于基于传统程序逻辑的验证器而言，内联（及展开）保持验证特性：若程序在特定注释下通过无界验证，则内联后的程序也能通过验证。这意味着在内联程序中检测到的任何错误都能揭示原始程序中的真实缺陷。然而，这一关键性质在自动分离逻辑验证器（如Caper、GRASShopper、RefinedC、Steel、VeriFast及基于Viper的验证器）中可能不成立。在此场景下，内联通常会改变方法执行所拥有的资源，这会影响自动证明搜索算法并引入虚假错误。本文提出首个面向自动分离逻辑验证器的保持验证内联技术。我们识别出程序的语义条件，并在Isabelle/HOL中证明该条件能确保最先进的自动分离逻辑验证器实现保持验证的内联。同时证明了其对偶结果：内联程序通过验证说明存在方法和循环注释，可支持原始程序的有界执行验证。为自动检查该语义条件，我们提出两种近似方法，分别通过语法检查和程序验证器实现。我们在Viper中实现这些检查，并证明其对来自不同验证器的非平凡示例有效。