ISSN 1000-1239 CN 11-1777/TP

Journal of Computer Research and Development ›› 2016, Vol. 53 ›› Issue (5): 1086-1094.

### Solving Cost Prediction Based Search in Symbolic Execution

Liu Jingde1,3, Chen Zhenbang1, Wang Ji1,2

1. 1(College of Computer, National University of Defense Technology, Changsha 410073); 2(Science and Technology on Parallel and Distributed Processing Laboratory (College of Computer, National University of Defense Technology), Changsha 410073); 3(95835 PLA Troops, Bayingolin, Xinjiang 841700)
• Online:2016-05-01

Abstract: 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.

CLC Number: