Unbounded Symbolic Execution for Program Verification

Symbolic execution with interpolation is emerging as an alternative to

cegar

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.

cegar

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

eager subsumption

, 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

selective unrolling

, that is, the unrolling of a loop along relevant paths only.