机械化定理证明研究综述
作者:
作者单位:

作者简介:

江南(1976-),女,湖北武汉人,博士,副教授,CCF专业会员,主要研究领域为可信软件,机器证明,编程语言;李清安(1986-),男,博士,副教授,CCF专业会员,主要研究领域为编译优化,程序分析,嵌入式系统;汪吕蒙(1988-),男,硕士,主要研究领域为CPU+GPU异质系统架构,GPGPU功耗优化;张晓瞳(1989-),男,硕士,主要研究领域为可信软件,可信编译,软件缺陷预测;何炎祥(1952-),男,博士,教授,博士生导师,CCF会士,主要研究领域为可信软件,分布式并行处理,高性能计算.

通讯作者:

何炎祥,E-mail:yxhe@whu.edu.cn

中图分类号:

TP18

基金项目:

国家自然科学基金(90818018,91018009,61170022,91118003,61373039);华为技术有限公司合作项目(YB2015090035);湖北工业大学校博士科研启动基金(BSQD2017043)


Overview on Mechanized Theorem Proving
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (90818018, 91018009, 61170022, 91118003, 61373039); HuaweiTechnologies Co. Ltd Project (YB2015090035); Doctoral Research Startup Foundation of Hubei University of Technology (BSQD2017043)

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    随着现代社会计算机化程度的提高,与计算机相关的各种系统故障足以造成巨大的经济损失.机械化定理证明能够建立更为严格的正确性,从而奠定系统的高可信性.针对机械化定理证明的逻辑基础和关键技术,详细剖析了一阶逻辑和基于消解的证明技术、自然演绎和类型化的λ演算、3种编程逻辑、基于高阶逻辑的硬件验证技术、程序构造和求精技术之间的联系和发展变迁,其中,3种编程逻辑包括一阶编程逻辑及变体、Floyd-Hoare逻辑和可计算函数逻辑.然后分析、比较了各类主流证明助手的设计特点,阐述了几个具有代表性的证明助手的开发和实现.接下来对它们在数学、编译器验证、操作系统微内核验证、电路设计验证等领域的应用成果进行了细致的分析.最后,对机械化定理证明进行了总结,并提出面临的挑战和未来研究方向.

    Abstract:

    Modern society is now being increasingly computerized. Computer-related failures could result in severe economic loss. Mechanized theorem proving is an approach to ensuring stricter correctness, and hence high trustworthiness. First, the logical foundations and key technologies of mechanized theorem proving are discussed. Specifically, first-order logic and resolution-based technology, natural deduction and Curry-Howard correspondence, three logics of programming including first-order programming logic and its variant, FloydHoare logic, and logic for computable functions, hardware verification technology based on higher-order logic, and program constructions and refinement are analyzed, as well as the relationship and evolvement between them. Then key design features of the mainstream proof assistants are compared, and the development and implementation of several representative provers are discussed. Next their applications in the fields of mathematics, compiler verification, operating-system microkernel verification, and circuit design verification are analyzed. Finally, mechanized theorem proving is summarized and challenges and future research directions are put forward.

    参考文献
    相似文献
    引证文献
引用本文

江南,李清安,汪吕蒙,张晓瞳,何炎祥.机械化定理证明研究综述.软件学报,2020,31(1):82-112

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2018-07-20
  • 最后修改日期:2019-03-04
  • 录用日期:
  • 在线发布日期: 2019-08-12
  • 出版日期: 2020-01-06
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号