Regular Property Guided Dynamic Symbolic Execution
Authors:
- Yufeng ZhangYZYufeng Zhang
- Zhenbang ChenZCZhenbang Chen
- Ji WangJWJi Wang
- Wei DongWDWei Dong
- Zhiming LiuZLZhiming Liu
- 1 May 2015
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- Vol. 1 (02705257) , 643-653
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
This publication has 40 references indexed in Scilit:
- Steering symbolic execution to less traveled paths2013
- Fast algorithms for Dyck-CFL-reachability with applications to alias analysis2013
- An Incremental Points-to Analysis with CFL-Reachability2013
- Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution2012
- A brief account of runtime verificationThe Journal of Logic and Algebraic Programming, 2009
- Mop2007
- Path Optimization in Programs and Its Application to Debugging2006
- Combining test case generation and runtime verificationTheoretical Computer Science, 2005
- Finite state description of communication protocolsComputer Networks (1976), 1978
- Symbolic execution and program testingCommunications of the ACM, 1976