一句话：为基于符号执行的渐进验证给出形式化与可靠性证明，并发现修复实现中的可靠性缺陷。
渐进验证允许显式部分规约，并通过静态与动态检查结合进行验证，使验证更增量并更早反馈。此前基于最弱前置条件的抽象方法虽已证明可靠，但对运行时检查的实现与优化指导不足；近期用符号执行实现渐进验证，但其可靠性（以及基于隐式动态帧的相关静态检查器）仍悬而未决。本文形式化了符号执行、优化的运行时检查生成与运行时执行，并证明该方法是可靠的；证明还覆盖 Viper 工具的核心子集，而此前尚无该子集的可靠性结果。该形式化还帮助发现一个已实现渐进验证工具中的可靠性缺陷，并描述了使其可靠所需的修复。
Gradual verification, which supports explicitly partial specifications and verifies them with a combination of static and dynamic checks, makes verification more incremental and provides earlier feedback to developers. While an abstract, weakest precondition-based approach to gradual verification was previously proven sound, the approach did not provide sufficient guidance for implementation and optimization of the required run-time checks. More recently, gradual verification was implemented using symbolic execution techniques, but the soundness of the approach (as with related static checkers based on implicit dynamic frames) was an open question. This paper puts practical gradual verification on a sound footing with a formalization of symbolic execution, optimized run-time check generation, and run time execution. We prove our approach is sound; our proof also covers a core subset of the Viper tool, for which we are aware of no previous soundness result. Our formalization enabled us to find a soundness bug in an implemented gradual verification tool and describe the fix necessary to make it sound.
@article{paperbot2642,
title = {Sound Gradual Verification with Symbolic Execution},
author = {Conrad Zimmerman and Jenna DiVincenzo and Jonathan Aldrich},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632927}
}