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

H and = S H at all iterations which execute line 7. When Dash cannot

generate a test case that supports a non yet supported abstract state, the model
is refined by removing the unfeasible abstract transitions, thus ensuring progress
of either abstract state space exploration or test case generation in the following
steps.
Dash is based on several synergies: FRS (feeding of reachable states) from
testing to symbolic exploration:

S

S sy := S S sy ; S sy := S sy ∪ S sy ,

and from testing to abstract exploration:

S H S H ; S H := S H := S H ,

CR (constraining by region) from abstract exploration and testing to symbolic
exploration:

H φ new := ( S H ∧¬ S ) ⇒ ,

FA (frontier abduction) to testing:

S := φ ∧ φ new ⊆ ; S := S ∪ S,

and RUR (refinement by unreachable region) from symbolic exploration to ab-
stract exploration:

op,− ; S H := H

r := ¬ wlp( p, ¬ φ new ); H := H ∪{ r } ; O H := O S .

5 Quantifying the Advantage of Synergies

Section 4 defined synergies between techniques, proposed a simple taxonomy of
synergies, and discussed the different synergies by means fo three state-of-art
approaches. A taxonomy is a key step towards comparing different approaches
both qualitatively and quantitatively. To quantifying the advantage of combined
techniques, we must put special care in isolating the effects of a specific compo-
nent among the others, in identifying techniques that do not leverage the synergy
to compare against, and in choosing appropriate metrics.
This section reports our preliminary insight about quantifying the perfor-
mance gain that the joint use of frontier abdution and feeding of reachable states
(FA+FRS) may introduce into an abstract exploration, with respect to tech-
niques that perform the abstract exploration statically. The value of FA+FRS
can be paramount because the satisfiability checks (required by abstract static
analyses to guarantee soundness and avoid false-positive results) is the most
expensive step, since the SAT problem is NP complete in the general case [8].
Many papers that discuss and experiment with static analyses, report that the
time complexity of the algorithms is dominated by the calls to the automatic
solver [14]. Combined techniques guarantee the satisfiability of the abstract
traces by construction, and thus eliminate such performance costs.