| 黄达明,曾庆凯.基于分离逻辑的程序验证技术.软件学报,2009,20(8):2051-2061 |
| 基于分离逻辑的程序验证技术 |
| Program Verification Techniques Based on Separation Logic |
| 投稿时间：2008-09-29 修订日期：2009-04-10 |
| DOI： |
| 中文关键词: 可信软件 程序验证 霍尔逻辑 分离逻辑 定理证明 |
| 英文关键词:trusted software program verification Hoare logic separation logic theorem proving |
| 基金项目: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 (高等学校博士学科点专项科研基金) |
|
| 摘要点击次数: 7001 |
| 全文下载次数: 7248 |
| 中文摘要: |
| 介绍了分离逻辑的验证原理和特点及其在程序验证方面的应用实例,分析了为支持程序验证的若干分离逻辑研究进展,包括分离逻辑的自身属性、与其他逻辑的关系、对程序语言和设计模式的支持以及定理证明器等内容.指出了分离逻辑进一步深入应用所面临的问题和解决方向. |
| 英文摘要: |
| 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. |
|
HTML 下载PDF全文 查看/发表评论 下载PDF阅读器 |
