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