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

ExploreDepthBounded( p , I , O ,maxDepth):
-- maxDepth > 0 is an integer, the maximum depth of the exploration

S := I
depth := 0
loop:
if S ⊆ O return INCORRECT
if depth ≥ maxDepth return INCONCLUSIVE else depth := depth + 1
S := Post( p, S )
if

S ⊆ S

return CORRECT

S ∪ S S

:=

ExploreWidthBounded( p , I , O ,maxWidth):
-- maxWidth > 0 is an integer, the maximum width of the exploration
( − ) ⊆ := some reductive function s.t. |S ⊆ | =min( maxWidth ,S )
S := I ⊆
exact := ( S = I )
loop:
if S ⊆ O return INCORRECT
S := Post( p, S ) ⊆
exact := exact ( S =Post( p, S ) ) ∧

S ⊆ S :
if exact return CORRECT else return INCONCLUSIVE

if

S ∪ S

S

:=

ExploreNonmonotone( p , I , O ):
S := I

loop:
if S ⊆ O return INCORRECT
S := Post( p, S )
if

S ⊆ S

return CORRECT

S − S S

:=

Fig. 3. Reduced state space exploration

end of the spectrum, an adverse oracle may discard computations leading to error
states and retain diverging correct computations. In this case, width-bounded
exploration converges less well and is less precise than full exhaustive exploration.
We choose not to make any assumption on how sampling selects states, which
reflects practical situations where no a priori knowledge exists about either the
program's reachable state space, or sampling. Consistently, the procedure in
Figure 3 produces an INCONCLUSIVE answer whenever the sampling misses some
states. This yields a procedure which is always less precise (but may converge
better) than full exhaustive exploration. Width bounds allow to limit the size
of S but not the size of S , for which either depth bounds or nonmonotony are
necessary.
Non-monotonic exploration focuses on minimizing the memory occupation of
a possibly exhaustive search, rather than limiting the scope of the exploration.
The rationale is that if the the reachability space of a program is large, a same
state will unlikely be visited twice. On this rationale, non-monotonic explo-
ration trades the cost in time of exploring some states more than once, against