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.

翻译：渐进式验证支持显式部分规格说明，并通过静态与动态检查相结合的方式进行验证，使得验证过程更具增量性，并为开发者提供更早的反馈。此前，基于最弱前置条件的抽象渐进式验证方法虽已被证明是可靠的，但该方法未能为所需运行时检查的实现与优化提供充分指导。近期，有研究采用符号执行技术实现了渐进式验证，但其可靠性（如同基于隐式动态框架的静态检查器一样）仍是一个悬而未决的问题。本文通过形式化符号执行、优化运行时检查生成及运行时执行，为实用化的渐进式验证奠定了可靠基础。我们证明了该方法具有可靠性；该证明还覆盖了Viper工具的核心子集——据我们所知，此前该工具尚未有可靠性结论。我们的形式化工作帮助发现了一个已实现渐进式验证工具中的可靠性缺陷，并描述了使其可靠所需的修复方案。