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

2. Symbolically execute in-depth the program along a path in M ,bychecking
for each branching point the satisfiability of a branch (say b 1 )outofthe
two possible branches b 1 and b 2 ;If b 1 is satisfiable, proceed the execution
through b 1 , else proceed through b 2 ;Update M by tagging all the feasible
and unfeasible branches on the path;
3. Identify a path to a never executed, potentially feasible branch b , with all
predecessors tagged as feasible, in the same order as for concolic exploration;
stop if no such branch exists;
4. Decide whether the path condition along the path to b identified at step 3
is satisfiable; If it is not, annotate b as infeasible along the path, otherwise,
annotate b as feasible along the path. Iterate from step 3.
To compare the two classes of approaches, we assume that both symbolic and
concolic explorations select program paths and branches in the same order
(steps 2-3 in both cases referring to the descriptions above). The path explo-
ration order of concolic execution depends on the test cases generated by a solver
as solutions of a satisfiability problem. Since the solver may pick different solu-
tions, the exploration order may vary if we repeat multiple times the analysis of
the same program. The exploration order of static symbolic exploration depends
on the analyzer that may freely decide which branch to explore first. However,
for all directed testing explorations of a program, there exists a global symbolic
execution that explores the program paths in the same order. By assuming the
same exploration order for the two approaches, we aim to eliminate the effect of
the exploration order on performance.
We quantify the performance of the different approaches as the number of calls
to the theorem prover. Since all branching points of the class of deterministic pro-
grams that we consider lead to either one or two feasible paths, a pure symbolic
execution calls the prover as most twice for each branching point. When both
branches are feasible (two-way branching point), two calls are necessary—one
call to confirm the feasibility of each branch. When one of the branches is infea-
sible (one-way branching point), pure symbolic execution calls the solver either
once or twice, depending on whether or not the infeasible branch is discovered
first, and thus the feasibility of the other path can be directly inferred without
the need of the second theorem prover call. We conservatively assume that both
cases can happen with 50% probability, independently on the evaluation order of
branches. The concolic approach, on the other hand, calls the prover only once
for each branching point, since the feasibility of one of the branches derives from
the fact that has been covered by the concrete execution, and is thus a benefit
of the FRS synergy.
Under the above assumptions, we can compute both the average number
of calls to the solver during static symbolic execution ( SolverCalls Static )and
during concolic execution ( SolverCalls Concolic ), and the relative gain G that
derives from FA+FRS. Let B 1 way and B 2 way be the number of one- and two-
way branching points analyzed so far, respectively, we have: