摘要
介绍了分离逻辑的验证原理和特点及其在程序验证方面的应用实例,分析了为支持程序验证的若干分离逻辑研究进展,包括分离逻辑的自身属性、与其他逻辑的关系、对程序语言和设计模式的支持以及定理证明器等内容.指出了分离逻辑进一步深入应用所面临的问题和解决方向.
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.
出处
《软件学报》
EI
CSCD
北大核心
2009年第8期2051-2061,共11页
Journal of Software
基金
国家自然科学基金Nos.60773170
60721002
90818022
国家高技术研究发展计划(863)No.2006AA01Z432
高等学校博士学科点专项科研基金No.200802840002~~
关键词
可信软件
程序验证
霍尔逻辑
分离逻辑
定理证明
trusted software
program verification
Hoare logic
separation logic
theorem proving
