Sparse Symbolic Loop Execution (Registered Report)

Dynamic symbolic execution is a powerful program analysis technique but is often limited by the path-explosion problem, particularly in the presence of heavily branching loops. In this paper, we introduce sparse symbolic loop execution (SSLE), a novel approach aimed at mitigating this issue. SSLE observes the edge patterns of sibling states, spawned from the same loop, at program branches up to a pre-computed loop-impact barrier. States that exhibit unique patterns of taken edges are selected for further exploration, while others are postponed. We implemented SSLE in a prototype called SparKLE and evaluated it on a set of 8 benchmarks against the popular symbolic execution engine KLEE. SSLE shows promising results and could increase line coverage by up to 55% in 1h runs using a depth-first-search heuristic. In other cases up to 99.997% of states could be postponed without any loss in coverage. Our planned evaluation will include a diverse set of 50 real-world benchmarks and will aim to better understand the effectiveness of SparKLE in handling symbolic loops, and how it compares with less complex approaches.