模型检测是一种形式化验证技术,主要用于系统的建模和分析。随着软件系统规模和复杂性的增加,模型检测中的状态爆炸问题愈发严重。为了改善该问题,目前应用较为广泛的解决方案是反例引导的抽象精化(Counterexample-guided Abstraction Refinement,CEGAR)静态检测方法。CPAChecker作为一种成功的模型检测工具,也引入了CEGAR静态检测方法,用于实现其谓词检测功能。在CPAChecker中,CEGAR静态检测方法虽然可以缓解状态爆炸问题,但是仍然存在两点不足。其一,以变量类型转换为代表的多类型问题,只有通过相关程序的动态执行才能得到变量的准确值;其二,验证程序模型时,静态检测技术需要遍历模型中的所有路径,并且需要针对每个反例调用精化算法进行分析。而在CPAChecker中引入动态执行操作,可以减少遍历路径的数量,消除不必要的精化操作。基于上述思想,本文提出了一种基于CPAChecker的动态程序验证方法,并给出了实现。基于CPAChecker的动态程序验证方法在CPAChecker中的静态检测方法的基础上加入了动态执行操作。对程序进行建模时,将待检测程序转换为控制流自动机(Control-Flow Automata,CFA),并根据CFA中分支结点的确定性或非确定性,在动态执行和抽象静态检测之间切换。当CFA中出现分支结点时,如果相关变量可确定,则使用动态执行操作来判断并分析该结点的唯一后继;如果相关变量不能确定,则调用静态检测方法分析该结点的后继。为了充分发挥动态执行的优点,本方法在遇到反例路径时,优先判断该路径中是否存在非确定结点。不存在非确定结点时,无需对该路径进行分析就可以判断程序不安全;存在非确定结点时,则需要对该反例进行分析。因此,本方法可以减少CFA中需要遍历的路径数量,并且可以减少反例路径的分析和精化次数。本方法使用静态检测技术减小了程序模型的规模,使用动态执行降低了静态检测的误判率,并减少了遍历路径和反例的数量,在一定程度上提高了CPAChecker的检测效率。