Abstract

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 talk, I 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.

Talk @ 3rd International Fuzzing Workshop (FUZZING 2024).