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