On the Integration of Software Testing and Formal Analysis - Empirical Software Engineering and Verification - page 164

The procedure converges on all the incorrect programs, and on the correct pro-
grams with finite-depth reachable state space 3 . This asymmetry is a bit an-
noying, since most interesting programs have not a finite-depth reachable state
space, and is a hallmark of dynamic techniques such as testing.

3.2 Reducing the Exploration Scope

Even if we assume convergence (when the state space is finite), the fully exhaus-
tive state space exploration is impractical, as the typical size of a program state
space quickly explodes also for relatively simple programs. Many techniques work
around the state-explosion problem by discarding some of the information dis-
covered during the exploration according to one of the following three strategies:

depth-bounded exploration, which consists in observing only finite compu-
tations and prefixes of computations, up to some predefined length.
width-bounded exploration, which consists in analyzing a subset of the states
discovered at a given exploration step.
non-monotonic exploration, which consists in forgetting the states discov-
ered at previous iterations, and retaining only the states at the current ex-
ploration depth.

Figure 3 presents the pseudocode for reduced state space exploration techniques.
In the figure, we write ( − ) ⊆ : P ( S ) →P ( S ) to indicate a nontrivial reductive

function, i.e., having the properties:

S ⊆ ⊆ S, S = ∅ implies S ⊆ = ∅ .

Informally, S ⊆ returns a nonempty subset of S (unless S is empty).
Depth-bounded exploration always converges, which can be considered a prac-
tical advantage by itself. On the other hand, whenever an error state does not
exist within the depth bound, an INCONCLUSIVE answer is mandatory to preserve
soundness. In other words, depth-bounded exploration is void w.r.t. correct pro-
grams with a reachable state space deeper than the bound. As an example, all
the programs with a finite reachable state space (for instance, finite state au-
tomata) fall in this class whenever the state space has size greater than the depth
bound.
Width-bounded exploration is hardly comparable with full exhaustive one.
Under some assumptions, it may even be more precise than the latter w.r.t.
some classes of programs. This happens when we assume that an optimal oracle
performs sampling by discarding as many correct diverging computations as
possible, and by retaining (when it exists) at least one incorrect computation.
In this case, width-bounded exploration converges better than full exhaustive
exploration w.r.t. some classes of correct programs with finite computations, and
produces a conclusive answer on all the inputs where it converges. At the opposite

3 A program's reachable state space has finite depth

n (from I )whenitis

0 ≤k<n Post k ( p, I ).