基于可满足性模理论求解器的程序路径验证方法  

Method of program path validation based on satisfiability modulo theory solver

作　　者：任胜兵[1] 吴斌[1] 张健威[1] 王志健[1] 

机构地区：[1]中南大学软件学院,长沙410005

出　　处：《计算机应用》2016年第10期2806-2810,共5页journal of Computer Applications

基　　金：国家自然科学基金资助项目(61272151);中南大学研究生自主探索创新项目(2016zzts374)~~

摘　　要：针对程序中因存在路径条数过多或复杂循环路径而导致路径验证时的路径搜索空间过大,直接影响验证的效率和准确率的问题,提出一种基于可满足性模理论(SMT)求解器的程序路径验证方法。首先利用决策树的方法对复杂循环路径提取不变式,构造无循环控制流图(NLCFG);然后通过基本路径法对控制流图(CFG)进行遍历,提取基本路径信息;最后利用SMT求解器作为约束求解器,将路径验证问题转化为约束求解问题来进行处理。与同样基于SMT求解器的路径验证工具CBMC和FSoft-SMT相比,该方法在对测试集程序的验证时间上比CBMC降低了25%以上,比FSoft-SMT降低了15%以上;在验证精度上,该方法有明显的提升。实验结果表明,方法可以有效解决路径搜索空间过大的问题,同时提高路径验证的效率和准确率。In programs, the path search space is too large because there are too many paths or complicated cycle paths, which directly affect the efficiency and accuracy for path validation. To resolve the above problem, a new program path validation method based on the Satisfiability Modulo Theory （SMT） solver was proposed. Firstly, loop invariants were extracted from the complicated cycle paths by using the method of decision tree, then the No-Loop Control Flow Graph （NLCFG） was constructed. Secondly, the information for basic paths was extracted via traversing Control Flow Graph （CFG） by using basic path method. Finally, the problem of path validation was converted into the problem of constraint solving by using a SMT solver as a constraint solver. Compared with CBMC and FSoft-SMT which were also based on SMT solver, the proposed method reduced validation time on test programs by more than 25% and 15% respectively. As for verification accuracy, the proposed method had significantly improvement. Experimental results show that this method can efficiently resolve the problem with too large path search space, and improve the efficiency and accuracy of path validation.

关 键 词：路径验证 控制流图 决策树 基本路径 可满足性模理论求解器 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]