Current static verification techniques support a wide range of programs. However, such techniques only support complete and detailed specifications, which places an undue burden on users. To solve this problem, prior work proposed gradual verification, which handles complete, partial, or missing specifications by soundly combining static and dynamic checking. Gradual verification has also been extended to programs that manipulate recursive, mutable data structures on the heap. Unfortunately, this extension does not reward users with decreased dynamic checking as specifications are refined. In fact, all properties are checked dynamically regardless of any static guarantees. Additionally, no full-fledged implementation of gradual verification exists so far, which prevents studying its performance and applicability in practice. We present Gradual C0, the first practicable gradual verifier for recursive heap data structures, which targets C0, a safe subset of C designed for education. Static verifiers supporting separation logic or implicit dynamic frames use symbolic execution for reasoning; so Gradual C0, which extends one such verifier, adopts symbolic execution at its core instead of the weakest liberal precondition approach used in prior work. Our approach addresses technical challenges related to symbolic execution with imprecise specifications, heap ownership, and branching in both program statements and specification formulas. We also deal with challenges related to minimizing insertion of dynamic checks and extensibility to other programming languages beyond C0. Finally, we provide the first empirical performance evaluation of a gradual verifier, and found that on average, Gradual C0 decreases run-time overhead between 11-34% compared to the fully-dynamic approach used in prior work. Further, the worst-case scenarios for performance are predictable and avoidable.

翻译：当前静态验证技术支持广泛的程序，但这类技术仅支持完整且详细的规范，这给用户带来了过重的负担。为解决此问题，先前工作提出了渐进式验证，通过将静态检查与动态检查进行可靠组合，处理完整、部分或缺失的规范。该技术已被扩展至能够操作堆上递归可变数据结构的程序，但这一扩展并未在规范逐步细化时相应减少动态检查：实际上，无论静态保证如何，所有性质均通过动态方式验证。此外，目前尚无完整的渐进式验证实现，阻碍了对其性能及实际应用性的研究。本文提出Gradual C0——首个面向递归堆数据结构的实用渐进式验证器，其目标语言为C0（专为教育设计的C语言安全子集）。支持分离逻辑或隐式动态框架的静态验证器采用符号执行进行推理；因此，Gradual C0扩展了此类验证器，其核心采用符号执行而非先前工作中的最弱前置条件方法。我们的方法解决了与以下方面相关的技术挑战：非精确规范下的符号执行、堆所有权机制，以及程序语句与规范公式中的分支结构。同时，我们处理了最小化动态检查插入及向C0以外编程语言扩展的挑战。最后，我们提供了首个渐进式验证器的实证性能评估，发现Gradual C0相比先前工作中的全动态方法，平均降低运行时开销11%-34%；且最差性能场景可预测且可规避。