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

is always updated by feeding reachable states from S .Theset S is initialized
with a set of initial states that represent random test input (line 2), and S is a
selection of a nontrivial subset of Post( p, S ) (line 5). If such a subset does not
exist ( S ⊆

S ), the approach generates new test inputs from S sy by frontier

abduction (lines 7-9).
The approach adds new reachable symbolic states with a Post co operator that
is defined by means of a new symbolic state transition relation that requires
successors to be supported by some set of concrete states S :

)
−−−→
S

( f,g

( σ ,γ )iff σ = σ, γ = γ

( σ, γ ) f ∧ g σ and

γ s = true for some s ∈ S .

As we can see, the new symbolic state transition relation requires the target
path condition be satisfied by a concrete state in S (thus simplifying the com-
putation). The corresponding Post co operator can be easily defined as follows:

( σ, γ ) p

Post co ( p, T, S ) de = ( σ ,γ ) ( σ ,γ )

{ ∈ S sy | − S } ,

( σ,γ ) ∈T

− S sy from the concrete to the
symbolic state space that selects the smallest set of symbolic states that are sup-
ported by a corresponding concrete one. By defining

and can be interpreted as an abstraction operator

de =Post co ( p, S sy ,S ),
the FRS (feeding of reachable states) nature of concolic execution is captured
by the sequence of operations:

S S sy

S sy := S S sy ; S sy := S sy ∪ S sy .

The loop in Figure 10 (lines 3-11) first computes the successors of the reachable
symbolic states S sy by exploiting the symbolic post-state transformer (line 7).
This is the computationally most expensive step of the whole procedure, but it
is inevitable to overcome the fact that testing is width-bounded. Then, it builds
the frontier as a predicate satisfied by all the concrete post-states of

S sy that

are not in , selects some concrete frontier states, and abduces them to form

the set of concrete post-states S (line 9). This last step ensures progress, since
it forces the execution of a sequence of statements different from the sequences
executed until then. The procedure is based on the assumption that a firing
sequence that produces an error state, produce only error states. Under this
assumption, we can stop exploring symbolic states as soon as we find a non-
erroneous concrete state in their extensions. The FA (frontier abduction) nature
of concolic execution is captured by the sequence of statements:

S sy

S := φ ∧¬ ⊆ ; S := S − φ S.

Directed testing and classic symbolic execution share the goal of increasing code
coverage, but direct testing is more effective, because while classic symbolic
execution needs to prove the feasibility of each branch along the explored paths,