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

针对程序中因存在路径条数过多或复杂循环路径而导致路径验证时的路径搜索空间过大，直接影响验证的效率和准确率的问题，提出一种基于可满足性模理论（SMT）求解器的程序路径验证方法。首先利用决策树的方法对复杂循环路径提取不变式，构造无循环控制流图（NLCFG）；然后通过基本路径法对控制流图（CFG）进行遍历，提取基本路径信息；最后利用SMT求解器作为约束求解器，将路径验证问题转化为约束求解问题来进行处理。与同样基于SMT求解器的路径验证工具CBMC和FSoft-SMT相比，该方法在对测试集程序的验证时间上比CBMC降低了25%以上，比FSoft-SMT降低了15%以上；在验证精度上，该方法有明显的提升。实验结果表明，方法可以有效解决路径搜索空间过大的问题，同时提高路径验证的效率和准确率。

Method of program path validation based on satisfiability modulo theory solver

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.