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

摘要：

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

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

所属期刊栏目：43

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金60673126;Intel中国研究中心资助项目

在线出版日期：2007-08-20（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：99-102,114