基于分离逻辑的程序验证研究综述

来源：软件学报杂志2017年第8期北京时间：

作者：秦胜潮,许智武,明仲

单位：秦胜潮，深圳大学 计算机与软件学院, 广东 深圳 51806011,许智武，深圳大学 计算机与软件学院, 广东 深圳 51806002,明仲，深圳大学 计算机与软件学院, 广东 深圳 51806003

摘要：自20世纪60年代以来，虽然有Floyd-Hoare逻辑的出现，但使用形式化工具对命令式程序的正确性和可靠性进行自动验证，一直被认为是极具挑战性、神圣不可及的工作.20世纪末，由于更多科研的投入，特别是微软、IBM等大型公司研发部门的大量人力、物力的投入，程序验证方面在21世纪初取得了不少进展，例如用于验证空客代码无运行时错误的ASTRÉE工具、用于Windows设备驱动里关于过程调用的协议验证的SLAM工具.但这些工具并没有考虑动态创建的堆（heap）：ASTRÉE工具假设待验证代码没有动态创建的堆，也没有递归；SLAM假设待验证系统已经有了内存安全性.事实上，很多重要的程序，例如Linux内核、Apache、操作系统设备驱动程序等，都涉及到对动态创建堆的操作.如何对这类操作堆的程序（heap-manipulating programs）进行自动验证仍然是一个难题.2001年~2002年，分离逻辑（separation logic）提出后，其分离（separation）思想和相应的框（frame）规则使得局部推理（local reasoning）可以很好地应用到程序验证中.自2004年以来，基于分离逻辑对操作动态创建堆的程序进行自动验证方面的研究有了很大的进展，取得了很多令人瞩目的成果，例如SpaceInvader/Abductor，Slayer，HIP/SLEEK，CSL等工作.着重对这方面的部分重要工作进行阐述.

关键词：分离逻辑;程序分析;程序验证;内存安全性;功能正确性

基金资助：国家自然科学基金（61373033，61502308，61672358）；深圳市科技创新委员会基础研究项目（JCYJ201418193546117）