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

This section shows that, thanks to FA+FRS, combined exploration techniques
require less calls to constrain solvers than equivalent static techniques, and tries
to analytically quantify the difference. Similar quantifications can be provided for
the other synergies indicated in Section 4, thus leading to a complete comparison
of different approaches.
5.1 Directed Testing
Here we try to analytically quantify the benefit of FA+FRS when exploited for
directed testing, as in Dart and Cute [12,16], and we compare the results with
purely static global symbolic execution, as in Java PathFinder and Save [1,7].
To isolate the effects of FA+FRS and avoid the influences of the mutual effects
of different optimizations we draw (with no loss of generality) on the following
assumptions:
- We assume an ideal sound and complete prover and a fully deterministic
program;
- We assume that any other optimization that may derive from synergies other
than FA and FRS is switched off 12 ;
- We assume that the considered pure-static and static-dynamic analysis pro-
cedures explore the program paths in exactly the same order.
To be more precise, we refer to the following versions of the concolic and symbolic
exploration procedures presented in the previous sections:
Concolic exploration
1. Let M be an initially empty symbolic execution model of the program state
space, (the tree of all the static program paths with all branches along them
tagged as potentially feasible);
2. Concretely execute the program on an input and update M by tagging all
the branches on the path as feasible;
3. Identify a path to a potentially feasible and not-yet executed branch b ,with
all predecessors tagged as feasible; stop if no such branch exists;
4. Symbolically execute the program along the path to the branch b identified
at step 3, and solve the path condition to a satisfying assignment; If the
solver fails (returns unsatisfiable ), annotate b as infeasible along the path,
and iterate from step 3; Otherwise, iterate from step 2 by considering the
returned satisfying assignment as a new input.
Static symbolic exploration
1. Let M be a, initially empty, symbolic execution model of the program state
space, as for concolic exploration step 1;
12 For example, common concolic analyses use the values from concrete states
to simplify (approximate) the symbolic formulas of the corresponding symbolic
states [12,16]. We deliberately ignore this and other similar optimizations.