采用CPAChecker的动态程序验证  

Dynamic program verification via a CPAChecker

作　　者：段钊 刘锟龙 DUAN Zhao;LIU Kunlong(School of Computer Science and Technology,Xidian Univ.,Xi'an 710071,China;School of Electrical Engineering and Automaton,Hefei University of Technology,Anhui 230009,China)

机构地区：[1]西安电子科技大学计算机学院,陕西西安710071 [2]合肥工业大学电气与自动化工程学院,安徽合肥230009

出　　处：《西安电子科技大学学报》2019年第1期33-38,共6页Journal of Xidian University

基　　金：国家自然科学基金(61732013)

摘　　要：针对模型检测中状态空间爆炸问题,在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.

关 键 词：模型检测 抽象精化 动态执行 程序验证 状态空间爆炸 

分 类 号：TP302.7[自动化与计算机技术—计算机系统结构]