| 摘要: |
| 介绍了分离逻辑的验证原理和特点及其在程序验证方面的应用实例,分析了为支持程序验证的若干分离逻辑研究进展,包括分离逻辑的自身属性、与其他逻辑的关系、对程序语言和设计模式的支持以及定理证明器等内容.指出了分离逻辑进一步深入应用所面临的问题和解决方向. |
| 关键词: 可信软件 程序验证 霍尔逻辑 分离逻辑 定理证明 |
| DOI： |
| 分类号: |
| 基金项目: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 (高等学校博士学科点专项科研基金) |
|
| Program Verification Techniques Based on Separation Logic |
|
HUANG Da-Ming,ZENG Qing-Kai
|
| Abstract: |
| This paper introduces the verification theory of separation logic, characteristics of separation logic, and some successful applications of separation logic. Researches on separation logic to support program verification are analyzed, including the properties of separation logic, its relation to other logics, its support to programming languages and design patterns, and the theorem provers’ support to separation logic. The problems encountered when separation logic is applied more widely are pointed out, and the future research directions are discussed. |
| Key words: trusted software program verification Hoare logic separation logic theorem proving |
