Compatible Branch Coverage Driven Symbolic Execution for Efficient Bug Finding

Symbolic execution is a powerful technique for bug finding by generating test inputs to systematically explore all feasible paths within a given threshold. However, its practical usage is often limited by the path explosion problem. In this paper, we propose compatible branch coverage driven symbolic execution for efficient bug finding. Our new technique owns a novel path-pruning strategy obtained from program dependency analysis to effectively avoid unnecessary explorations. Specifically, based on a Compatible Branch Set , our technique directs symbolic execution to explore feasible branches while soundly pruning redundant paths that have no new contributions to branch coverage. We have implemented our approach atop KLEE and conducted experiments on a set of programs from Siemens Suite, GNU Coreutils, and other real-world programs. Experimental results show that, compared with the state-of-the-art symbolic execution techniques, our approach always uses significantly less time to reproduce bugs while achieving the same or better branch coverage. On average, our approach got over 45% path reduction and 3x speedup on the GNU Coreutils programs