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

SolverCalls Static = B 1 way
2

+2 B 1 way
2

+2 B 2 way ,

SolverCalls Concolic = B 1 way + B 2 way ,
and consequently:

B 1 way
2

G = SolverCalls Static − SolverCalls Concolic = + B 2 way .

We can then conclude that the gain is always positive, and depends on the
number of one- and two-way branching points of the program. The structure of
the program state space strongly affects the yield of FA+FRS—the “narrower”
the program state space is, the more symbolic states a test case is able to discover
on average, and thus the less must be discovered by invoking the solver.

5.2 Dynamic Abstract Interpretation
Here we try to quantify the benefit of FA+FRS as exploited in Yorsh-Ball-
Sagiv [18], and compare it with purely static abstract interpretation used to
build a (possibly optimal) abstract trasformer, as done for example by Slam [2].
As in the former case, we assume an ideal sound and complete prover, a fully
deterministic program, the presence of no synergies other than FA+FRS, and
the same order of exploration of the abstract program states.
To be more precise, we refer to the following versions of the static/dynamic
and static procedures presented in the previous sections:
Static/dynamic abstract exploration
1. Let S A be a set of abstract states initialized to a possibly empty set of the
initial abstract states;
2. Concretely execute the program with an input, and extend S A with the
abstract states supported by the concrete states reached during the concrete
execution;
3. Solve the constraints associated to the abstract states up to a satisfying
assignment sp( p, S A ) ∧¬ S A ; If the solver fails (returns unsatisfiable ),
stop; Otherwise, iterate from step 2 by considering the returned satisfying
assignment as a new input.

Static abstract exploration
1. Let S A be a set of abstract states initialized to a possibly empty set of the
initial abstract states;
2. Solve the constraints associated to the abstract states up to a satisfying as-
signment sp( p, ; If solver fails (returns unsatisfiable ), stop;

Otherwise add the abstract state supported by the returned satisfying as-
signment to S A , and iterate this step.
As above, we assume that the static/dynamic and the static abstract approaches
explore abstract state in the same order. Under these assumptions, the static ap-
proach calls the solver once at each step to compute each abstract state except
for the initial ones, and once at the end to verify the transitive closure. Thus, if

S A ) ∧¬ S A