Abstract

Dynamic symbolic execution is a powerful program analysis tech- nique 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 eight benchmarks against the popular symbolic execution engine KLEE. SSLE shows promising results and could increase line coverage by up to 55% in 1 h 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.