Computer Engineering and Applications ›› 2007, Vol. 43 ›› Issue (21): 99-102.
• 产品、研发、测试 • Previous Articles Next Articles
LIU Cheng，CHEN Yi-yun，GE Lin，HUA Bao-jian
Received:
Revised:
Online:
Published:
Contact:
刘 诚，陈意云，葛 琳，华保健
通讯作者:
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
摘要： 出具证明编译器是随着人们对现今的软件提出更高的可靠性和安全性要求而产生的工具，它结合了以往程序设计和程序安全性证明的技术。论文介绍了一个出具证明编译器原型系统的实现。
关键词: 软件安全, 出具证明编译器, 验证条件, 形式化证明方法, 证明生成器
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.
刘 诚，陈意云，葛 琳，华保健. 一个出具证明编译器原型系统的实现[J]. 计算机工程与应用, 2007, 43(21): 99-102.
0 / Recommend
Add to citation manager EndNote|Ris|BibTeX
URL: http://cea.ceaj.org/EN/
http://cea.ceaj.org/EN/Y2007/V43/I21/99
