【摘要】：自20世紀60年代以來,雖然有Floyd-Hoare邏輯的出現(xiàn),但使用形式化工具對命令式程序的正確性和可靠性進行自動驗證,一直被認為是極具挑戰(zhàn)性、神圣不可及的工作.20世紀末,由于更多科研的投入,特別是微軟、IBM等大型公司研發(fā)部門的大量人力、物力的投入,程序驗證方面在21世紀初取得了不少進展,例如用于驗證空客代碼無運行時錯誤的ASTRéE工具、用于Windows設備驅(qū)動里關于過程調(diào)用的協(xié)議驗證的SLAM工具.但這些工具并沒有考慮動態(tài)創(chuàng)建的堆(heap):ASTRéE工具假設待驗證代碼沒有動態(tài)創(chuàng)建的堆,也沒有遞歸;SLAM假設待驗證系統(tǒng)已經(jīng)有了內(nèi)存安全性.事實上,很多重要的程序,例如Linux內(nèi)核、Apache、操作系統(tǒng)設備驅(qū)動程序等,都涉及到對動態(tài)創(chuàng)建堆的操作.如何對這類操作堆的程序(heap-manipulating programs)進行自動驗證仍然是一個難題.2001年~2002年,分離邏輯(separation logic)提出后,其分離(separation)思想和相應的框(frame)規(guī)則使得局部推理(local reasoning)可以很好地應用到程序驗證中.自2004年以來,基于分離邏輯對操作動態(tài)創(chuàng)建堆的程序進行自動驗證方面的研究有了很大的進展,取得了很多令人矚目的成果,例如Space Invader/Abductor,Slayer,HIP/SLEEK,CSL等工作.著重對這方面的部分重要工作進行闡述.

【相似文獻】

相關期刊論文 前10條

1 胡久清;何炎祥;李衛(wèi)華;;程序驗證機械化的進一步探討[J];電子計算機動態(tài);1981年09期

2 陸奇,張福波,錢家驊;程序分片:其改進算法與在程序驗證中的應用[J];計算機學報;1988年04期

3 周青;;關于程序驗證方法的討論[J];計算機科學;1995年03期

4 何志林;用Visual Basic程序驗證杜西結(jié)論——兼談推廣結(jié)論[J];運城高等�？茖W校學報;2001年03期

5 李衛(wèi)華;程序驗證中的簡化技巧[J];計算機學報;1983年02期

6 葛湘川;孫永強;;一個實驗性機械程序驗證系統(tǒng)[J];上海交通大學學報;1982年02期

7 李衛(wèi)華;;定理證明與程序驗證[J];計算機科學;1982年01期

8 劉定飛;鐘珞;;支持程序驗證的模塊方法[J];計算機科學;1994年01期

9 賈國平,鄭國梁;一個統(tǒng)一的程序驗證框架[J];軟件學報;1997年02期

10 李彥恒;孟志強;樊景森;;VB程序驗證成礦元素線性相關性[J];科技資訊;2006年17期

相關博士學位論文 前6條

1 徐鳴;程序驗證與系統(tǒng)分析中的若干符號計算問題[D];華東師范大學;2010年

2 雷紅軒;量子程序驗證中若干問題研究[D];陜西師范大學;2013年

3 武斌;基于符號計算方法的程序驗證技術(shù)研究[D];華東師范大學;2010年

4 邢建英;程序驗證關鍵技術(shù)研究[D];國防科學技術(shù)大學;2011年

5 易曉東;面向C程序驗證的切片執(zhí)行方法[D];國防科學技術(shù)大學;2006年

6 李勇;基于軟件事務內(nèi)存的并行程序驗證[D];中國科學技術(shù)大學;2011年

相關碩士學位論文 前3條

1 冬雨辰;用于交互式程序驗證的數(shù)據(jù)流分析技術(shù)[D];南京大學;2016年

2 聞曉;一種基于Mealy機的BPEL程序驗證模型研究[D];西南大學;2009年

3 章程;VeriJava中靜態(tài)驗證器的設計與實現(xiàn)[D];上海交通大學;2007年

，

本文編號：2581114