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

A small catalog of synergies. Here we introduce a simple catalog of the synergies
we detected by surveying the recent literature. We will use the taxonomy in the
next section to characterize the different examples.
- Feeding of reachable states (FRS) : A technique soundly feeds a translation
of some of its reachable states into a coarser one. This is usually done to
reduce the exploration chore of the coarser technique by providing it with
information about the program state space that has already been computed,
albeit at a different granularity (in which case the latter can delegate search
on the uncovered abstract states to a finer technique by frontier abduction,
FA);
- Frontier abduction (FA) : A technique feeds part of its frontier 6 into a finer
technique, to delegate to the latter technique the exploration of the abduced
frontier slice. The advantage may stem either because the finer technique is
more ecient than the coarser one in exploring the frontier (in which case the
results are afterwards ported to the coarser technique by FRS), or because
the coarser technique may continue the analysis when the finer technique is
stuck by invariance in an inconclusive way;
- Refinement by unreachable region (RUR) : Whenever an abstract region R
is proved unreachable from a region Q by a more precise technique, the
abstraction of the coarser technique can be refined by superimposing to
it any set of predicates sucient for showing the region unreachable (for
instance, a predicate whose extension is precisely Q).
- Constraining by region (CR) : A technique constrains a finer one to analyze
an abstract region it has detected. This is usually done when an abstract
technique is stuck by reachability in an inconclusive way, and allows to deter-
mine feasible behaviours within the abstract region. It is typically followed
by either FA (for eciently searching within the region when some feasible
behaviour exists) or RUR (when the region is unfeasible);
- Formula construction by satisfiability (FCS) : Whenever a symbolic technique
must build a satisfiable formula from a set of clauses, it can exploit the
existence of a concrete state which satisfies some of them to build it, or some
relaxation of it. This has at least two applications: building a short formula
from a long one (useful while performing refinement), and building a formula
that can be solved automatically from a formula that cannot (useful while
performing frontier abduction).
4.3 Detecting Synergies in Combined Techniques: A Brief Survey
Here we survey popular approaches that combine different testing, static analysis
and formal verification techniques, with the goal of exemplifying the different
possible synergies.
6 With the word frontier we indicate a region of the state space which a technique has
discovered, but of which has not yet calculated the successors. This loose definition
is consistent with the many uses of the word in the related literature.