Symbolic execution with interpolation is emerging as an alternative to
for software verification. The performance of both methods relies critically on interpolation in order to obtain the most general abstraction of the current symbolic or abstract state which can be shown to remain error-free.
naturally handles unbounded loops because it is based on abstract interpretation. In contrast, symbolic execution requires a special extension for such loops.
In this paper, we present such an extension. Its main characteristic is that it performs
, that is, it always attempts to perform abstraction in order to avoid exploring redundant symbolic states. It balances this primary desire for more abstraction with the secondary desire to maintain the
strongest loop invariant
, for earlier detection of infeasible paths, which entails less abstraction. Occasionally certain abstractions are not permitted because of the reachability of error states; this is the underlying mechanism which then causes
, that is, the unrolling of a loop along relevant paths only.