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

作者：黄达明; 曾庆凯

来源：软件学报, 2009, (08): 2051-2061.

• 可信软件
• 程序验证
• 霍尔逻辑
• 分离逻辑
• 定理证明 trusted software
• program verification
• Hoare logic
• separation logic
• theorem proving

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

• 单位
  计算机软件新技术国家重点实验室; 南京大学