Using State Merging and State Pruning to Address the Path Explosion Problem Faced by Symbolic Execution

摘要

Symbolic execution is a promising technique to discover software vulnerabilities and improve the quality of code. However, symbolic execution su ers from a path explosion problem where the number of possible paths within a program grows exponentially with respect to loops and conditionals. New techniques are needed to address the path explosion problem. This research presents a novel algorithm which combines the previously researched techniques of state merging and state pruning. A prototype of the algorithm along with a pure state merging and pure state pruning are implemented in the KLEE symbolic execution tool with the goal of increasing the code coverage. Each algorithm is tested over 66 of the GNU COREUTILS utilities. State merging combined with state pruning outperforms the unmodified version of KLEE on 53% of the COREUTILS. These results confirm that state merging with pruning has viability in addressing the path explosion problem of symbolic execution.