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

发布时间：2020-02-19 20:32

【摘要】：自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年以来,基于分离逻辑对操作动态创建堆的程序进行自动验证方面的研究有了很大的进展,取得了很多令人瞩目的成果,例如Space Invader/Abductor,Slayer,HIP/SLEEK,CSL等工作.着重对这方面的部分重要工作进行阐述.

【相似文献】

相关期刊论文 前10条

1 胡久清;何炎祥;李卫华;;程序验证机械化的进一步探讨[J];电子计算机动态;1981年09期

2 陆奇,张福波,钱家骅;程序分片:其改进算法与在程序验证中的应用[J];计算机学报;1988年04期

3 周青;;关于程序验证方法的讨论[J];计算机科学;1995年03期

4 何志林;用Visual Basic程序验证杜西结论——兼谈推广结论[J];运城高等专科学校学报;2001年03期

5 李卫华;程序验证中的简化技巧[J];计算机学报;1983年02期

6 葛湘川;孙永强;;一个实验性机械程序验证系统[J];上海交通大学学报;1982年02期

7 李卫华;;定理证明与程序验证[J];计算机科学;1982年01期

8 刘定飞;钟珞;;支持程序验证的模块方法[J];计算机科学;1994年01期

9 贾国平,郑国梁;一个统一的程序验证框架[J];软件学报;1997年02期

10 李彦恒;孟志强;樊景森;;VB程序验证成矿元素线性相关性[J];科技资讯;2006年17期

相关博士学位论文 前6条

1 徐鸣;程序验证与系统分析中的若干符号计算问题[D];华东师范大学;2010年

2 雷红轩;量子程序验证中若干问题研究[D];陕西师范大学;2013年

3 武斌;基于符号计算方法的程序验证技术研究[D];华东师范大学;2010年

4 邢建英;程序验证关键技术研究[D];国防科学技术大学;2011年

5 易晓东;面向C程序验证的切片执行方法[D];国防科学技术大学;2006年

6 李勇;基于软件事务内存的并行程序验证[D];中国科学技术大学;2011年

相关硕士学位论文 前3条

1 冬雨辰;用于交互式程序验证的数据流分析技术[D];南京大学;2016年

2 闻晓;一种基于Mealy机的BPEL程序验证模型研究[D];西南大学;2009年

3 章程;VeriJava中静态验证器的设计与实现[D];上海交通大学;2007年

，

本文编号：2581114