Coq中用于基于高阶逻辑定理证明、提升自动化一致性与可复用性的通用形式化内存框架
编程语言
2018-03-28 v3
摘要
近年来,许多轻量级程序被部署于关键领域,例如基于区块链技术的智能合约。因此,此类程序的安全性和可靠性应由最可信的技术来保证。高阶逻辑定理证明是验证程序性质最可靠的技术之一。然而,程序可能由不同的高级编程语言开发,而一个能够同时支持不同形式化验证规范(尤其在代码层面)、通用、可扩展且可复用的形式化内存(GERM)框架目前尚不存在用于验证程序性质。因此,本工作提出一个GERM框架以填补此空白。该框架模拟物理内存硬件结构,包括底层形式化内存空间,并提供一组简单、非侵入式的应用程序接口及辅助工具,使用Coq可同时支持不同的形式化验证规范。所提GERM框架独立且可定制,并完全在Coq中验证。我们还提出了Curry-Howard同构的一个扩展,记为执行-验证同构(EVI),它将符号执行与定理证明结合,以提高高阶逻辑定理证明辅助工具的自动化程度。我们还以广义代数数据类型风格实现了一门玩具函数式编程语言,以及基于GERM框架在Coq中的一个形式化解释器。这些实现随后被用于演示EVI在一个简单代码片段上的应用。
引用
@article{arxiv.1803.00403,
title = {A general formal memory framework in Coq for verifying the properties of programs based on higher-order logic theorem proving with increased automation, consistency, and reusability},
author = {Zheng Yang and Hang Lei},
journal= {arXiv preprint arXiv:1803.00403},
year = {2018}
}
备注
27 pages, 28 figures