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

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

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

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

中国科学技术大学计算机科学技术系，合肥 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

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

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

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

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

刘诚，陈意云，葛琳，华保健. 一个出具证明编译器原型系统的实现[J]. 计算机工程与应用, 2007, 43(21): 99-102.

LIU Cheng，CHEN Yi-yun，GE Lin，HUA Bao-jian. Implementation of certifying compiler prototype[J]. Computer Engineering and Applications, 2007, 43(21): 99-102.

[1]	强小辉，陈波，陈国凯. OpenSSL HeartBleed漏洞分析及检测技术研究[J]. 计算机工程与应用, 2016, 52(9): 88-95.
[2]	陈智勇1，2，徐锋1，2，余萍1，2. 一个基于COP的控制软件安全性增强方法[J]. 计算机工程与应用, 2013, 49(5): 64-69.