Gradual Program Verification
Gradual Program Verification
复制标题
渐进式程序验证
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
É. Tanter
中科院分区：
文献类型：
--
作者：
J. Bader;Jonathan Aldrich;É. Tanter
单独考虑时，静态和动态程序验证方法都有明显的缺点。受渐进打字研究的启发，我们提出渐进验证以无缝灵活地结合静态和动态验证。借鉴抽象解释的一般原则，特别是最近 Garcia 等人的抽象渐进打字方法，我们系统地从静态验证系统中推导出渐进验证系统。这种方法通过构造产生了一个渐进的验证系统，该系统与原始静态系统兼容，但在需要时通过诉诸动态验证来克服其刚性。与渐进式打字一样，程序员可以通过调整前置条件和后置条件的（im）精度来控制静态和动态检查之间的权衡。渐进验证系统的形式语义及其属性证明，包括 Siek 等人的渐进保证，已经在 Coq 证明助手中完全机械化。
Both static and dynamic program verification approaches have significant disadvantages when considered in isolation. Inspired by research on gradual typing, we propose gradual verification to seamlessly and flexibly combine static and dynamic verification. Drawing on general principles from abstract interpretation, and in particular on the recent Abstracting Gradual Typing methodology of Garcia et al., we systematically derive a gradual verification system from a static one. This approach yields, by construction, a gradual verification system that is compatible with the original static system, but overcomes its rigidity by resorting to dynamic verification when desired. As with gradual typing, the programmer can control the trade-off between static and dynamic checking by tuning the (im)precision of pre- and postconditions. The formal semantics of the gradual verification system and the proofs of its properties, including the gradual guarantees of Siek et al., have been fully mechanized in the Coq proof assistant.