Effective interactive proofs for higher-order imperative programs
Effective interactive proofs for higher-order imperative programs
复制标题
高阶命令式程序的有效交互式证明
DOI：
10.1145/1596550.1596565
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Ryan Wisnesky
中科院分区：
文献类型：
--
作者：
A. Chlipala;G. Malecha;Greg Morrisett;Avraham Shinnar;Ryan Wisnesky
我们提出了一种新的方法来构建和验证高阶，命令式程序使用Coq证明助手。我们建立在过去的工作Ynot系统，这是基于霍尔类型理论。最初的系统是一个概念验证，每个程序验证都是通过费力的手动验证完成的，许多代码都用于无趣的底层细节。在本文中，我们提出了一个重新实现的Ynot，这使得有可能实现充分验证，高阶命令式程序与合理的证明负担。同时，我们的新系统完全在Coq源文件中实现，展示了证明助手作为语言设计和验证研究平台的多功能性。这两个版本的系统进行了评估与案例研究，在验证必要的数据结构，如哈希表与高阶迭代器。与旧系统相比，我们的新系统中的验证负担至少减少了一个数量级，通过用自动化代替手动证明。自动化的核心是高阶分离逻辑中隐含的简化过程，它带有钩子，允许程序员添加特定于域的简化规则。
我们认为我们的基础设施的有效性，通过验证一些数据结构和packrat解析器，我们比较类似的努力在其他项目。与数据结构验证的竞争方法相比，我们的系统包含的必须可信的代码要少得多;也就是说，大约有一百行Coq代码定义了程序逻辑。我们所有的定理和决策过程都有或建立了机器可检查的正确性证明，从第一原则，消除了工具错误的机会，创造错误的验证。
We present a new approach for constructing and verifying higher-order, imperative programs using the Coq proof assistant. We build on the past work on the Ynot system, which is based on Hoare Type Theory. That original system was a proof of concept, where every program verification was accomplished via laborious manual proofs, with much code devoted to uninteresting low-level details. In this paper, we present a re-implementation of Ynot which makes it possible to implement fully-verified, higher-order imperative programs with reasonable proof burden. At the same time, our new system is implemented entirely in Coq source files, showcasing the versatility of that proof assistant as a platform for research on language design and verification. Both versions of the system have been evaluated with case studies in the verification of imperative data structures, such as hash tables with higher-order iterators. The verification burden in our new system is reduced by at least an order of magnitude compared to the old system, by replacing manual proof with automation. The core of the automation is a simplification procedure for implications in higher-order separation logic, with hooks that allow programmers to add domain-specific simplification rules.
We argue for the effectiveness of our infrastructure by verifying a number of data structures and a packrat parser, and we compare to similar efforts within other projects. Compared to competing approaches to data structure verification, our system includes much less code that must be trusted; namely, about a hundred lines of Coq code defining a program logic. All of our theorems and decision procedures have or build machine-checkable correctness proofs from first principles, removing opportunities for tool bugs to create faulty verifications.