一句话：提出首个用于自动分离逻辑验证器的保持验证内联技术，并给出经 Isabelle/HOL 验证的语义条件。
有界验证通过内联调用与展开循环，可尽量减少方法规约和循环不变式。但对自动分离逻辑验证器（如 Caper、Viper 等），内联会改变方法执行拥有的资源，影响自动证明搜索并可能引入伪错误，因此传统程序逻辑中内联保持验证的性质未必成立。本文提出首个用于此类验证器的保持验证内联技术：定义程序上的语义条件，在 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.
@article{paperbot2045,
title = {Verification-Preserving Inlining in Automatic Separation Logic Verifiers},
author = {Thibault Dardinier and Gaurav Parthasarathy and Peter Müller},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA1},
year = {2023},
doi = {10.1145/3586054}
}