Abstract

Some static analysis tools can produce partial traces through programs under analysis annotated with conditions that the analyser believes are important for a bug to trigger. A dynamic symbolic execution tool may be able to exploit the trace by (a) guiding the search heuristically so that paths that follow the trace most closely are prioritised for exploration, and (b) pruning the search using the conditions associated with each step of the trace. This may allow the bug to be quickly confirmed using dynamic symbolic execution. This talk presents our results by combining off-the-shelf static analysers with KLEE.

Joint work with Pritam Gharat, Cristian Cadar, and Alastair F. Donadson.