Title :
Regular Property Guided Dynamic Symbolic Execution
Author :
Yufeng Zhang ; Zhenbang Chen ; Ji Wang ; Wei Dong ; Zhiming Liu
Author_Institution :
Key Lab. of High Performance Comput., Nat. Univ. of Defense Technol., Changsha, China
Abstract :
A challenging problem in software engineering is to check if a program has an execution path satisfying a regular property. We propose a novel method of dynamic symbolic execution (DSE) to automatically find a path of a program satisfying a regular property. What makes our method distinct is when exploring the path space, DSE is guided by the synergy of static analysis and dynamic analysis to find a target path as soon as possible. We have implemented our guided DSE method for Java programs based on JPF and WALA, and applied it to 13 real-world open source Java programs, a total of 225K lines of code, for extensive experiments. The results show the effectiveness, efficiency, feasibility and scalability of the method. Compared with the pure DSE on the time to find the first target path, the average speedup of the guided DSE is more than 258X when analyzing the programs that have more than 100 paths.
Keywords :
Java; program diagnostics; public domain software; software engineering; symbol manipulation; JPF; WALA; dynamic symbolic execution; execution path; guided DSE method; path space; real-world open source Java programs; regular property; software engineering; static analysis; synergy; Algorithm design and analysis; Context; History; Java; Monitoring; Software engineering; Space exploration; Dynamic Analysis; Dynamic Symbolic Execution; Finite State Machine; Regular Property; Static Analysis;
Conference_Titel :
Software Engineering (ICSE), 2015 IEEE/ACM 37th IEEE International Conference on
Conference_Location :
Florence
DOI :
10.1109/ICSE.2015.80
