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

Directed testing. Directed testing aims to exercise all executable control-flow
paths of a program under test systematically and automatically [12,16,17]. 7 In
directed testing, a controller supervises the generation of test cases to ensure
that new test cases exercise control-flow paths not-yet-executed.
Directed testing uses a technique called dynamic symbolic execution ,or con-
colic execution 8 that combines concrete execution of test cases with symbolic
execution along the same execution paths. It starts with a set of randomly gen-
erated test inputs, and iterates through concolic execution and test input genera-
tion. While executing test cases, concolic execution produces the path conditions
that represent the executed paths. The controller exploits these path conditions
to generate new test cases that execute unexplored paths. It first identifies a
branching point that contains a not-yet-executed branch in the executed paths
(if none, the analysis terminates since all executable paths have been explored).
Then, it considers all the clauses in a path condition up to that branching point,
and negates the last clause to obtain a path condition that correspond to a not-
yet-executed branch. Finally, it solves the identified path condition to generate
a new test input (if none, the branch is infeasible, and the controller tries to
identify another candidate not-yet-executed branch).

1

ExploreConcolic( p , I , O ):

2 S I ⊆ S sy := { (id ,init ) } init ∈ E s.t. init = I

:= ; for some

3

loop:

4 S ⊆ O

if return INCORRECT

S := Post( p, S ) ⊆ 5

S ⊆ S :

6 if

φ := sp( p, φ ) 7 φ := S sy ;

φ = ⇒ φ 8 if return CORRECT

S := φ ∧¬φ ⊆

9

S sy := Post co ( p, S sy ,S ) 10

S − S S sy ∪ S sy S S sy

11 := ; :=

Fig. 10. Concolic execution

Figure 10 illustrates the concolic execution approach underlying directed test-
ing approaches, recast on the reachability problem. The presentation abstracts
from details like the order of the visit of the concrete state space, to focus on
the main characteristics of the approach, thus accounting for all the features
invariant across the different implementations available in literature.
The approach in Figure 10 maintains a set of reachable concrete states, S ,
and a set of reachable symbolic states, S sy . The set of concrete states is updated
by either concrete execution or test input generation, the set of symbolic states

7 In practice, this goal often implies exercising as many paths as possible up to some
predefined testing budget, since the number of control-flow paths is infinite for most
programs.
8 Concolic = conc rete + symb olic .