• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Mathematically structured functional programming >Foundational Program Verification in Coq with Automated Proofs
【24h】

Foundational Program Verification in Coq with Automated Proofs

机译：Coq中带有自动证明的基础程序验证

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Most people who know of the proof assistant Coq associate it with long, manual proofs via tactic scripts. In contrast, classical verification tools, based on automated theorem-provers for first-order logic, are well established as supporting program verification without any manual proof steps. However, there is a price to pay: program verifiers are large, complex bodies of code, and believing their outputs requires believing in much more than the correct implementation of Coq's proof-checking kernel.rnIn this tutorial, I will demonstrate how to use the Bedrock Coq library to get the best of both worlds. Our focus will be on the kinds of programs with the most tedious detail and the most opportunity to benefit from automation: namely, those written inrnassembly language. I will show how to build automated correctness proofs of simple imperative data structures, while dealing with first-class code pointers and producing Coq proof terms for theorems whose statements depend on little beyond operational semantics of machine code.
机译：大多数了解证明助手Coq的人都通过战术脚本将其与冗长的手动证明相关联。相反，基于用于一阶逻辑的自动定理证明器的经典验证工具已经很好地建立为支持程序验证，而无需任何手动验证步骤。但是，需要付出一定的代价：程序验证者是大型，复杂的代码体，并且相信它们的输出所需要的不仅仅是真正实现Coq的证明检查内核。在本教程中，我将演示如何使用基岩Coq库充分发挥了两者的优势。我们的重点将放在最繁琐的细节和从自动化中受益最多的程序上，即那些使用汇编语言编写的程序。我将展示如何构建简单命令式数据结构的自动正确性证明，同时处理一流的代码指针并为定理产生Coq证明条件，这些定理的陈述几乎不依赖于机器代码的操作语义。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号