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

Now we discuss more in detail how synergies may cope with the main sources
of ineciency and incompleteness for static and dynamic techniques. The dis-
cussion is informal, and is better substantiated later in this section through the
analysis of a number of examples from recent literature.
Trading off over- and under-approximation. As highlighted in Section 3, prac-
tical techniques reason on the program state space by approximation, in the
forms of either over-approximation, which is void w.r.t. incorrect programs, or
under-approximation, which is void w.r.t. correct programs. Modern techniques
rely at the same time on both over- and under-approximating exploration of
the state space. The combination of the two forms of approximation can im-
prove the exploration of the state space when each one guides the other. Under-
approximating techniques can benefit from techniques that reason on the state
space at a coarser grain, since they provide hints for accelerating the finer explo-
ration towards regions of the state space more likely to contain an error state.
Dually, when a concrete analysis proves that a region is free from erroneous be-
haviours, the over-approximated exploration can progress beyond this infeasible
region, thus improving completeness.
Improving performance of symbolic reasoning. Static techniques are based on
symbolic reasoning that underlies their expressiveness, but reduces performance
and completeness. For example, symbolic execution requires deciding whether a
symbolic post-state has an empty extension, in which case the symbolic state
is pruned. Failing in pruning infeasible symbolic states may lead to unnecessary
exploration and false alarms. Exploration based on predicate abstraction requires
deciding whether an abstract states is unreachable from any of the abstract
states that we could not prove unreachable. The cost of not proving that an
abstract state is unreachable is a degradation of the precision of the model,
which may at worst become unusable. Both procedures require to decide whether
some symbolic formulas are satisfiable, a problem undecidable for most logical
languages, and computationally hard for all the others. The consequence is that
symbolic reasoning is a source of either incompleteness, or performance loss, or
both.
A simple way of reducing the amount of invocations of a decision procedure is
by exploiting concrete states. A concrete state implicitly proves satisfiable all the
formulas that evaluate true in it (together with the negation of all the formulas
that evaluate to false ). Therefore the concrete states generated by a dynamic
technique can be used to prove satisfiable the formulas arising from a static one.
This approach is potentially useful since dynamic techniques are very ecient
generators of concrete states, albeit with bias towards depth rather than width
of exploration. Even when a state does not satisfy a formula of interest, it may
satisfy some of its subformulas. Some techniques exploit this fact either to reduce
the complexity of a formula by weakening/strengthening it (whenever a weaker
or stronger formula than the original one is acceptable), or to build a candidate
solution of a complex formula from the solution of one of its subformulas.