采用CPAChecker的动态程序验证

Dynamic program verification via a CPAChecker

针对模型检测中状态空间爆炸问题,在CPAChecker的抽象谓词检测方法的基础上,提出了一种基于动态执行的检测方法.首先,根据程序的控制流程图,对程序进行静态检测。在静态检测的过程中,根据分支语句的确定性,利用动态执行的方法来加快检测的过程。其中,抽象检测可以有效地限制系统模型的规模,动态执行不仅可以有效地减少静态检测导致的误判,而且有助于引导构建精确的系统模型,降低虚假反例的数量和不必要的反例分析和精化。实验数据显示,这种算法明显提高了传统的反例引导谓词抽象精化算法的检测效率和准确率。

To overcome the state space explosion problem in model checking,a CPAChecker based dynamic program verification approach is proposed.The proposed approach first verifies the program statically by unwinding the control flow chart.In the process,dynamic execution is applied to accelerate the verification on the basis of the determinism of branch statements.Specifically,abstract verification effectively reduces the size of the system models,while dynamic detection not only effectively reduces false positives,but also guides the construction of more accurate system models.As a result,the proposed approach makes counterexample-guided abstraction refinement more efficient and accurate in practice.