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

• 作者: 李兆鹏 李隆 郭丽 陈意云
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: 高可信软件 安全程序 形式化证明方法 证明工具Coq
• 年，卷（期）: 2006,（21）
• 所属期刊栏目: 产品、研发、测试
• 页码范围: 64-67,73
• 页数: 5页
• 分类号: TP311
• 字数: 3652字
• 语种: 中文
• DOI: 10.3321/j.issn:1002-8331.2006.21.019

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈意云	中国科学技术大学计算机科学技术系	83	854	16.0	26.0
2	李隆	中国科学技术大学计算机科学技术系	6	40	3.0	6.0
3	李兆鹏	中国科学技术大学计算机科学技术系	17	99	7.0	9.0
4	郭丽	中国科学技术大学计算机科学技术系	12	72	4.0	8.0