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