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

directed testing discovers most branches by testing, and thus can safely assume
feasibility. As discussed in Section 5, directed testing can improve the eciency
up to 50% over classic symbolic execution, needing up to 50% less calls to an
external solver than classic symbolic execution.

Dynamic abstract interpretation. The dynamic abstract interpretation approach
proposed by Yorsh, Ball and Sagiv in 2006 and that we will refer to as the
Yorsh-Ball-Sagiv procedure is based on a combination of dynamic and static
analysis claimed to be more ecient than the traditional approach of statically
calculating the abstract transformer [18]. In a nutshell, the Yorsh-Ball-Sagiv
procedure aims to compute the most-precise abstract property with respect to
an abstraction, without explicitly computing the corresponding most-precise ab-
stract transformer. The Yorsh-Ball-Sagiv procedure is parametric with re-
spect to the categories of abstractions. Here we describe the Yorsh-Ball-Sagiv
procedure by assuming a predicate abstraction with predicates in H .
The Yorsh-Ball-Sagiv procedure alternates program execution and the-
orem proving. Whenever the program is executed for some (possibly random)
input, all traversed concrete states s are abstracted to the corresponding abstract
ones via a suitable abstraction map − H :

de =
s∈S

β H ( s ) de = {{h ∈ H | s | = h}},

S H β H ( s ) .

− H can be easily computed when S is finite (which is always the case with

testing) by evaluating all the predicates in H against all the concrete states in
S .TheYorsh-Ball-Sagiv procedure cumulates the abstract states incremen-
tally cumulated throughout concrete execution, to build the currently reached
abstract region. At any point of the analysis, for example when the execution
terminates or does not produce new abstract states, the current set of abstract
states can be checked for invariance, to understand whether it covers the reach-
able state space of the program under analysis. This check is done by querying a
theorem prover on whether any post-state of any concrete state in the computed
abstract region is still in the same region. If this is the case, the procedure can
terminate since it has computed an invariant for the program that covers its
reachable state space. Otherwise, there is at least one concrete state that can be
found by a suitable solver such that (1) it is not in the computed the abstract
region, and (2) it is a successor of some state in the computed abstract region.
Concrete execution of the program starting from such state feeds back a new
iteration of the analysis, possibly discovering new reachable abstract states.
Figure 11 illustrates the Yorsh-Ball-Sagiv procedure for an arbitrary ab-
straction A by referring to the reachability problem. The structure of the pro-
cedure shares the structure of concolic execution (Figure 10), reflecting the fact
that the two procedures work similarly. They compute a set of reachable states
with concrete execution, use the concrete states to build a set of abstract states,
and when the concrete execution is stuck because of inconclusive invariance,
they exploit frontier abduction to feed concrete execution of fresh states. Like
concolic execution, the Yorsh-Ball-Sagiv procedure has the nature of both