Mitigating Path Explosion in Dynamic Symbolic Execution via Memoisation, Sparse Loop Execution and Static Analysis-Guided Exploration

Symbolic execution is a powerful program analysis technique with applications in many domains. However, when analysing real-world applications, its scalability is often limited by two factors: the inherent constraint solving overhead and path explosion.

Memoised symbolic execution efficiently stores information about the ongoing analysis to disk, allowing users to quickly re-start symbolic execution runs and continue paths that were previously interrupted due to memory pressure or aggressively pruning search heuristics.

Sparse symbolic loop execution is a novel approach designed to mitigate path explosion caused by heavily-branching loops. Sibling states that were spawned from the same loop are classified by their behaviour at subsequent decision points. States that show a unique behaviour are kept, while others are sampled according to configurable strategies.

Static analysis-guided symbolic execution leverages bug reports from off-the-shelf static analysers to steer symbolic execution towards interesting and potentially buggy code sections. Static analysers produce a large number of bug reports, most of which are false positives in practice. A technique that can automatically confirm true positives among these reports would be highly beneficial to developers, allowing them to prioritise the most critical issues.

This talk is based on the following papers:

Frank Busse is a PhD student at Imperial College London. His research focuses on overcoming the limitations of symbolic execution and making it applicable in an industrial setting.