| 基于分离逻辑的程序验证技术 |
| |
| 引用本文： | 黄达明,曾庆凯.基于分离逻辑的程序验证技术[J].软件学报,2009,20(8):2051-2061. |
| |
| 作者姓名： | 黄达明 曾庆凯 |
| |
| 作者单位： | 南京大学,计算机软件新技术国家重点实验室,江苏,南京,210093;南京大学,计算机科学与技术系,江苏,南京,210093 |
| |
| 基金项目： | Supported by 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 (高等学校博士学科点专项科研基金) |
| |
| 摘 要： | 介绍了分离逻辑的验证原理和特点及其在程序验证方面的应用实例,分析了为支持程序验证的若干分离逻辑研究进展,包括分离逻辑的自身属性、与其他逻辑的关系、对程序语言和设计模式的支持以及定理证明器等内容.指出了分离逻辑进一步深入应用所面临的问题和解决方向.
|
| 关 键 词： | 可信软件 程序验证 霍尔逻辑 分离逻辑 定理证明 |
| 收稿时间： | 2008/9/29 0:00:00 |
| 修稿时间： | 2009/4/10 0:00:00 |
Program Verification Techniques Based on Separation Logic |
| |
| HUANG Da-Ming and ZENG Qing-Kai.Program Verification Techniques Based on Separation Logic[J].Journal of Software,2009,20(8):2051-2061. |
| |
| Authors: | HUANG Da-Ming and ZENG Qing-Kai |
| |
| Affiliation: | State Key Laboratory for Novel Software Technology;Nanjing University;Nanjing 210093;China;Department of Computer Science and Technology;China |
| |
| Abstract: | |
| |
| Keywords: | trusted software program verification Hoare logic separation logic theorem proving |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
