Staged symbolic execution

J. H. Siddiqui and S. Khurshid
ACM Symposium on Applied Computing — Software Verification and Testing Track (SAV-SVT 2012)


Recent advances in constraint solving technology and raw computation power have led to a substantial increase in the effectiveness of techniques based on symbolic execution for systematic bug finding. However, scaling symbolic execution remains a challenging problem. We present a novel approach to increase the efficiency of symbolic execution for systematic testing of object-oriented programs. Our insight is that we can apply symbolic execu- tion in stages, rather than the traditional 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 example, a class invariant can provide the basis of generating abstract symbolic tests that are then used to symbolically execute several methods that require their inputs to satisfy the invariant. We present an experimental evaluation to compare our approach against KLEE, a state-of-the-art implementation of symbolic execution. Results show that our approach enables significant savings in the cost of systematic testing using symbolic execution.
(SAC-SVT 2012), Riva del Garda (Trento), Italy, March 2012. (Acceptance rate: 27%, 12/43)


@inproceedings { sac2012,
author = { }, }