Exploiting Program Dependencies for Scalable Multiple-Path Symbolic Execution


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.

Related research categories:
(1) Symbolic Execution
(2) Symbolic Evaluation
(3) Program Analysis
(4) Control Dependence
(5) Data Dependence
(6) Testing

Go To Publications