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