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