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 pathexploration 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. Categories and Subject Descriptors: D.2.5 [Software Engineering]: Testing and Debugging—symbolic execution, testing tools; F.3.2 [Logics and Meanings of Pro...

• Type: Conference
• Year: 2010
• Where: ISSTA
• Authors: Raúl A. Santelices, Mary Jean Harrold
• Keywords: ISSTA 2010, Multiple-path Symbolic Execution, Software Engineering, SPD Exploits Control, Symbolic Execution