欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
位置：立项数据库 > 立项详情页
中文摘要：
在当今信息社会，关键软件的高可信成了保障国家安全、保持经济可持续发展和维护社会稳定的必要条件。其中安全性是关注的重点之一，软件满足安全策略的证明方法是研究的热点之一。本项目采用逻辑方法和类型方法相结合的方式，研究串行高级语言程序安全性的描述、证明、从高级语言级的安全性证明到目标语言级安全性证明的编译和在目标语言级进行安全性证明的检验的方法，解决该方法中主要的理论和技术问题，主要涉及指针逻辑、验证条件生成、自动定理证明、汇编语言级的证明框架、程序规范和程序性质证明的翻译等。主要成果包括（1）一种突出指针类型的小语言PointerC的指针逻辑；（2）能输出证明项的线性整数自动定理证明器和指针逻辑自动定理证明器；（3）Hoare逻辑风格的汇编程序的证明框架；（4）基于程序员提供函数前后断言和循环不变式的PointerC语言的出具证明编译器；（5）操作系统内核的部分模块、垃圾收集器和使用事务内存的并行程序的验证。这项研究对保证关键软件的安全性，对建设我国各种安全的信息系统有着重要作用。
结论摘要：
英文主题词high-confidence software; software safety and security; certifying compiler; program verification; pointer logic
成果综合统计
期刊论文
会议论文
专利
获奖
著作
期刊论文
会议论文
相关项目
陈意云的项目
