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