Exploiting program dependencies for scalable multiple-path symbolic execution
Raúl Santelices, Mary Jean Harrold · 2010
This paper presents a new technique, called Symbolic Program Decomposition (or SPD), for symbolic execution of multiple paths that is more scalable than existing techniques, which symbolically execute control-flow paths individually. SPD exploits control and data dependencies to avoid analyzing unnecessary combinations of subpaths. SPD can also compute an over-approximation of symbolic execution by abstracting away symbolic subterms arbitrarily, to further scale the analysis at the cost of precision. The paper also presents our implementation and empirical evaluation showing that SPD can achieve savings of orders of magnitude in the path-exploration costs of multiple-path symbolic execution. Finally, the paper presents a study that examines the use of SPD for a particular application: change analysis for test-suite augmentation.