Employing Run-time Static Analysis to Improve Concolic Execution

Dynamic symbolic execution, or concolic execution,
is a program testing technique that systematically executes a
program with the aim of exploring all feasible program paths,
and locating and reporting all errors encountered in these paths.
However, as the complexity of the program grows, the number of
program paths explodes, making it infeasible for concolic testers
to explore all of them. To reduce the number of paths to explore,
several concolic testing tools have recently started employing
static analysis to prune paths guaranteed by the static analysis
to be safe. The concolic tester must then only focus on those
paths that might contain an error, as reported by the analysis.
However, due to imprecisions in the analysis’ result, the reported
errors may just be false positives, and it is up to the tester to
verify whether a reported alarm is an actual error or merely a
false positive. In this position paper, we propose to increase the
precision of these analyses by not only performing an initial static
analysis before starting concolic testing of the program, but also
by launching incremental static analyses over the program at run
time, and incorporating into the analyses run-time information
observed by the tester. The increased precision that results from
incorporating such run-time information should enable further
pruning of the program paths that must be explored by the
concolic tester.