计算机工程与应用 ›› 2007, Vol. 43 ›› Issue (21): 99-102.

• 产品、研发、测试 • 上一篇    下一篇

一个出具证明编译器原型系统的实现

刘 诚,陈意云,葛 琳,华保健   

  1. 中国科学技术大学 计算机科学技术系,合肥 230027
  • 收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:2007-07-21 发布日期:2007-07-21
  • 通讯作者: 刘 诚

Implementation of certifying compiler prototype

LIU Cheng,CHEN Yi-yun,GE Lin,HUA Bao-jian   

  1. Department of Computer Science and Technology,University of Science and Technology of China,Hefei 230027,China
  • Received:1900-01-01 Revised:1900-01-01 Online:2007-07-21 Published:2007-07-21
  • Contact: LIU Cheng

摘要: 出具证明编译器是随着人们对现今的软件提出更高的可靠性和安全性要求而产生的工具,它结合了以往程序设计和程序安全性证明的技术。论文介绍了一个出具证明编译器原型系统的实现。

关键词: 软件安全, 出具证明编译器, 验证条件, 形式化证明方法, 证明生成器

Abstract: Certifying compiler is such a tool coming up with the increasing demands for higher reliability and safety of computer software.It combines the techniques in programming languages and program verifications.This paper describes some details in implementing our prototype of a certifying compiler.

Key words: software safety, certifying compiler, verification condition, formal proof method, proof generator