逐步验证展开表达式和纯函数
Gradually Verifying Unfolding Expressions & Pure Functions
浏览论文内容
中文总结 AI 辅助
本文针对使用符号执行的验证器，给出展开表达式和纯函数的形式语义并扩展到渐进验证器，提供健全性证明，支持Gradual C0，结果也适用于相关静态验证器，以此提高涉及所有权规范的模块化。
中文摘要 AI 辅助
展开表达式在评估依赖堆的表达式时临时展开谓词以利用其所属字段，纯函数是可用于规范的依赖堆函数。基于隐式动态框架的演绎程序验证器（如Gradual C0、Gobra、Nagini和SnaKt）使用它们来提高涉及所有权的规范的模块化。本文给出了使用符号执行的静态验证器中展开表达式和纯函数的形式语义，将其扩展到渐进验证器并提供了健全性证明。为支持Gradual C0，证明在渐进验证设置中进行，该结果也适用于使用符号执行的静态验证器。
英文摘要
Unfolding expressions, which temporarily unfold a predicate to leverage its owned fields when evaluating a heap-dependent expression, and pure functions, which are heap-dependent functions that can be used in specifications, are used in deductive program verifiers based on implicit dynamic frames, such as Gradual C0, Gobra, Nagini, and SnaKt, to increase the modularity of specifications involving ownership. In this paper, we present the formal semantics for unfolding expressions and pure functions for a static verifier using symbolic execution, extend it for a gradual verifier, and provide a proof of soundness. To support Gradual C0, our proof is in the setting of gradual verification, a deductive program verification system that combines static and dynamic verification to allow partial specifications. However, because the gradual verifier is a conservative extension of a static verifier, our results also apply to static verifiers that use symbolic execution, such as the Silicon symbolic execution backend for the Viper verification infrastructure used by Gobra, Nagini, and SnaKt.
