基于Coq构造携带证明的安全程序

摘要：

对可靠程序的需求随着高可信软件在信息社会中的作用日益重要而增加.基于形式化证明工具构造携带证明的安全程序,给出严格的程序规范及其证明是提高软件可靠性的重要途径.论文介绍使用形式化证明工具Coq构造安全程序的过程和经验.

关键词：高可信软件、安全程序、形式化证明方法、证明工具Coq

所属期刊栏目：42

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

资助基金：中国科学院资助项目60473068;Intel中国研究中心资助项目

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

页数：共5页

页码：64-67,73