Mitigating Path Explosion in Symbolic Execution via Branches Merging

摘要

Symbolic execution has been widely used to detect software vulnerability. Nevertheless, due to path explosion, the detection method with symbolic execution still struggles to achieve scalability. In symbolic execution, one way to reduce the number of paths that need to explore is to merge the different branches. In this paper, we present an approach to merge branches which could effectively mitigate the path explosion problem. The main idea of the approach is to reduce the redundancy of different paths during symbolic execution, different paths have different semantics but to the subsequent statements of these paths, they could be seen as one path or be merged into one path. According to the idea, we propose an algorithm and illustrate the algorithm with an example.