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

best practice suggests to uses various techniques based on different approxima-
tion criteria, to compensate the respective deficiencies. Some recent research
work shows that combining different techniques by sharing information about
the state space can increase the benefits of heterogeneity. This section reviews
some of the most popular approaches that combine techniques by sharing in-
formation about the state space, highlights the patterns that characterize the
information sharing, and pinpoints the relative advantages. In this way, we draft
a framework of the synergies between state exploration techniques as they are
enacted by modern combined approaches.
4.1 A Note on “Static” and “Dynamic” Techniques
While this paper focuses mostly on the interplay between static and dynamic
techniques, we do not explicitly characterized what makes a technique “static”
or “dynamic”, but we rely on the intuition that dynamic techniques refer to
direct program execution, while static techniques refer to reasoning over models
of program behaviour. We will assume that dynamic techniques are extensional,
concrete, nonmonotonic, width-bounded, and possibly depth-bounded. Testing,
the paradigmatic dynamic technique, has all these features, while the presence
of width bound rules out techniques as the explicit-state exploration performed
by the VeriSoft software model checker [11]. We assume that static techniques
are either symbolic or abstract, but we will not assume them to be monotonic,
width- or depth-unbounded.
4.2 Synergies between Techniques
Throughout this paper we consider synergies between state space exploration
techniques. Synergies arise when different state space exploration techniques
share or exchange information about the program state space. Sharing informa-
tion is necessary, but not sucient for igniting mutual synergies. For example, we
do not consider synergetic two techniques A and B, if B simply uses information
about the program state space produced by A. A synergy must also explain how
such knowledge is integrated into the state space exploration performed by B,
and how such integration contributes to improve the exploration chore of either
A, or B, or both.
Synergies between techniques can improve the trade-off between precision,
tractability and speed on the target of the analysis, often yielding combined
techniques with better convergence and eciency than their single components.
This happens because synergies may:
- Improve the knowledge of the program state space by fusing the knowledge
coming from different techniques.
- Accelerate the exploration of the program state space by delegating differ-
ent regions of the state space to the technique which may explore it more
eciently;