摘要
对可靠程序的需求随着高可信软件在信息社会中的作用日益重要而增加。基于形式化证明工具构造携带证明的安全程序,给出严格的程序规范及其证明是提高软件可靠性的重要途径。论文介绍使用形式化证明工具Coq构造安全程序的过程和经验。
As the high-trusted software plays more and more important role in today＇s information society,the requirement of sound programs greatly increases.To improve software soundness and security,it is a feasible approach for developers to strictly specify and prove programs safety properties based on formal proof tool.This paper describes the process and experience of building such security programs using proof assistant Coq.
出处
《计算机工程与应用》
CSCD
北大核心
2006年第21期64-67,73,共5页
Computer Engineering and Applications
基金
国家自然科学基金资助项目(编号:60473068)
Intel中国研究中心资助项目
