中文摘要：

符号执行中约束求解所占的时间比例非常高．同时，不同复杂度约束的求解时间开销差距悬殊，这一现象在对包含复杂数值计算的程序进行符号执行时尤为明显．在指定时间内求解更多约束有利于覆盖更多语句和探索更多路径．为此，提出了基于求解开销预测的符号执行搜索策略．基于实验总结出了度量约束复杂度的经验公式，并结合约束的历史求解开销来预测当前的求解开销，从而在符号执行过程中优先探索求解开销较小的路径．在 KLEE 中实现了上述搜索策略，并对 GNU 科学计算库（GSL ）中的12个模块进行了实验．实验结果表明，相比现有搜索策略，提出的搜索策略在保证语句覆盖率的同时，可以探索更多的路径（平均24．34％提高）；而且，在相同时间内，可以查找出更多的软件缺陷，同时查找出相同缺陷的时间开销平均降低了44．43％．

英文摘要：

In symbolic execution ,constraint solving needs a large proportion of execution time .The solving time of a constraint differs a lot with respect to the complexity ,which happens a lot when analyzing the programs with complex numerical calculations . Solving more constraints within a specified time contributes to covering more statements and exploring more paths .Considering this feature ,we propose a solving cost prediction based search strategy for symbolic execution .Based on the experimental data of constraint solving , we conclude an empirical formula to evaluate the complexity of constraints ,and predict the solving cost of a constraint combined with historical solving cost data .The formula is used in our strategy to explore the paths with a lower solving cost with a higher priority .We have implemented our strategy in KLEE ,a state-of-art symbolic executor for C , and carried out the experiments on the randomly selected 12 modules in GNU Scientific Library （GSL ） . The experimental results indicate that ： in a same period , compared with the existing strategy ,our strategy can explore averagely 24 .34% more paths ,without sacrificing the statement coverage ;and our strategy can find more bugs .In addition ,the time of using our strategy for finding same bugs decreases 44 .43% in average .