%0 Journal Article
%T 基于分离逻辑的程序验证研究综述
%A 明仲
%A 秦胜潮
%A 许智武
%J -
%D 2017
%R 10.13328/j.cnki.jos.005272
%X 自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等工作.着重对这方面的部分重要工作进行阐述
%K 分离逻辑 程序分析 程序验证 内存安全性 功能正确性
%U http://www.jos.org.cn/jos/ch/reader/view_abstract.aspx?file_no=5272&flag=1