摘要：針對模型檢測中狀態(tài)空間爆炸問題,在CPAChecker的抽象謂詞檢測方法的基礎(chǔ)上,提出了一種基于動態(tài)執(zhí)行的檢測方法.首先,根據(jù)程序的控制流程圖,對程序進(jìn)行靜態(tài)檢測。在靜態(tài)檢測的過程中,根據(jù)分支語句的確定性,利用動態(tài)執(zhí)行的方法來加快檢測的過程。其中,抽象檢測可以有效地限制系統(tǒng)模型的規(guī)模,動態(tài)執(zhí)行不僅可以有效地減少靜態(tài)檢測導(dǎo)致的誤判,而且有助于引導(dǎo)構(gòu)建精確的系統(tǒng)模型,降低虛假反例的數(shù)量和不必要的反例分析和精化。實驗數(shù)據(jù)顯示,這種算法明顯提高了傳統(tǒng)的反例引導(dǎo)謂詞抽象精化算法的檢測效率和準(zhǔn)確率。