Scaling symbolic execution using staged analysis.

J. H. Siddiqui and S. Khurshid
J. Innovations in Systems and Software Engineering (JISSE 2013)

Abstract

Recent advances in constraint solving tech- nology and raw computation power have led to a sub- stantial increase in the effectiveness of techniques based on symbolic execution for systematic bug finding. How- ever, scaling symbolic execution remains a challenging problem. We present a novel approach to increase the effi- ciency of symbolic execution for systematic testing of object-oriented programs. Our insight is that we can apply symbolic execution in stages, rather than the tra- ditional approach of applying it all at once, to compute abstract symbolic inputs that can later be shared across different methods to test them systematically. For ex- ample, a class invariant can provide the basis of gen- erating abstract symbolic tests that are then used to symbolically execute several methods that require their inputs to satisfy the invariant. We present an exper- imental evaluation to compare our approach against KLEE, a state-of-the-art implementation of symbolic execution. Results show that our approach enables sig- nificant savings in the cost of systematic testing using symbolic execution.
Volume 9, Issue 2 (2013), Page 119-131

BibTex

@inproceedings { jisse2013,
author = { }, }