摘要：隨著軟件的不斷更新迭代,軟件正確性檢測(cè)的必要性愈加凸顯,軟件正確性檢測(cè)的處理時(shí)間直接決定軟件的維護(hù)成本。動(dòng)態(tài)測(cè)試的斷言編寫(xiě)和靜態(tài)分析的符號(hào)執(zhí)行均針對(duì)程序正確性進(jìn)行優(yōu)化完善,但分析結(jié)果易出現(xiàn)路徑缺失甚至錯(cuò)誤無(wú)法識(shí)別等問(wèn)題?，F(xiàn)有驗(yàn)證方法在路徑擴(kuò)展時(shí)易生成較多無(wú)用路徑,且針對(duì)性不強(qiáng),因此有必要研究一種更為可靠的方案。本文采用最弱前置條件對(duì)軟件可行性加以分析,對(duì)程序執(zhí)行語(yǔ)義正確建模,使用程序切片技術(shù)預(yù)處理程序代碼,并根據(jù)層級(jí)結(jié)構(gòu)存儲(chǔ)節(jié)點(diǎn)及其子程序。實(shí)驗(yàn)結(jié)果表明,該方法可以有效減小靜態(tài)分析對(duì)程序狀態(tài)抽象操作帶來(lái)的驗(yàn)證精度損耗,且能夠遍歷求解出程序的所有可能路徑,并通過(guò)分組標(biāo)出條件表達(dá)式的結(jié)論真假值,以此驗(yàn)證路徑正確性,同時(shí)可對(duì)高復(fù)雜的程序代碼進(jìn)行有效的正確性分析。