Lazy Symbolic Execution and Enhanced Learning
Chu Duc Jiep, Joxan Jaffar and Vijayaraghavan Murali
Abstract
Symbolic execution with interpolation has emerged as a powerful technique for
software verification. Its performance heavily relies heavily on the
quality of the computed ``interpolants'', formulas which succinctly describe a
generalization of the symbolic states proved so far.
Symbolic execution by default is \emph{eager},
that is, execution along a symbolic path stops the moment when infeasibility is
detected in the logical constraints describing the path so far. This may
however hinder the discovery of better interpolants, i.e., more general
abstractions of the symbolic state which are yet sufficient ensure the entire
symbolic path remains error-free.
In this paper, we present a systematic method which speculates that an
infeasibility may be temporarily ignored in the pursuit of better information
about the path in question. This speculation does not lose the intrinsic
benefits of symbolic execution because its operation shall be bounded. We argue
that the trade-off between this `enhanced learning' and incurring additional cost
(which in principle may not be productive) is in fact in favor of speculation.
Finally, we demonstrate with a state-of-the-art system on realistic benchmarks
that this method enhances symbolic execution by a factor of 2 or more.