Current static verification techniques have allowed users to specify and verify more code than ever before. 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 exhibit a pay-as-you-go cost model, which rewards users with increased static correctness guarantees and decreased dynamic checking as specifications are refined. In fact, all properties are checked dynamically regardless of any static guarantees, resulting in significant run-time overhead. In this paper, we present the first gradual verifier for recursive heap data structures that can be used on real programs, called Gradual C0. Additionally, Gradual C0 reasons with symbolic execution and supports a pay-as-you-go cost model. Our approach addresses technical challenges related to symbolic execution with imprecise specifications, heap ownership, and that branches across program statements and specifications. Finally, we empirically evaluated the pay-as-you-go cost model of Gradual C0 and found that, on average, Gradual C0 decreases run-time overhead between 50-75% compared to the fully-dynamic approach used in prior work. Further, the worst-case scenarios for performance are predictable and avoidable.
翻译:目前静态的核查技术使用户能够比以往任何时候更能够指定和核查更多的代码。然而,这种技术只支持完整和详细的规格,给用户带来过重的负担。为了解决这个问题,先前的工作提议逐步核查,通过稳妥地结合静态和动态的检查来处理完整、部分或缺失的规格。渐进核查还扩大到操纵堆积上的循环变换数据结构的程序。不幸的是,这一扩展没有显示现收现付成本模式,这种模式奖励用户增加静态的正确性保证和随着规格的改进而减少动态检查。事实上,所有属性都受到动态检查,而不论任何静态的保证如何,从而导致大量运行时间的管理管理。在本文中,我们提出了可用于真实程序(称为 " 渐进式 " C0 " ) 的循环性重现数据结构的第一个渐进核查程序。此外,带有象征性执行和支持现收现付成本模式的渐进式C0理由。我们的方法处理与象征性执行有关的技术挑战,用不精确的规格、高压所有权,以及跨程序声明和规格的分支。最后,我们避免了50个周期性业绩模型和前期成本之间的全面评估。