基于分离逻辑的程序验证技术

摘要：

介绍了分离逻辑的验证原理和特点及其在程序验证方面的应用实例,分析了为支持程序验证的若干分离逻辑研究进展,包括分离逻辑的自身属性、与其他逻辑的关系、对程序语言和设计模式的支持以及定理证明器等内容.指出了分离逻辑进一步深入应用所面临的问题和解决方向.

关键词：可信软件、程序验证、霍尔逻辑、分离逻辑、定理证明

所属期刊栏目：20

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

资助基金：the National Natural Science Foundation of China under Grant Nos.60773170, 60721002, 90818022;the National High-Tech Research and Development Plan of China under Grant No.2006AA01Z432 国家高技术研究发展计划863;the Specialized Research Fund for the Doctoral Program of Higher Education of China under Grant No.200802840002

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

页数：共11页

页码：2051-2061