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

the final abstraction contains N abstract states out of which I are initial states
that do not result in a call to the solver, the static approach calls the solver
N

I + 1 times. The static/dynamic approach calls the solver once for each new
state, and once at the end to discover abstract invariance. It does not call the
solver for the 0

−

I reachable abstract states discovered by concrete
execution, thus resulting in a total of N

≤ C<N −

− I − C + 1 calls. In summary:

SolverCalls Static = N − I +1 ,

SolverCalls S/D = N − I − C +1 ,

and consequently:

G = SolverCalls Static − SolverCalls S/D = C.

The gain of the static/dynamic procedure over the purely static one is the num-
ber of abstract states discovered by concrete execution. This again depends on
the shape of the abstract state space: Narrow structures enable discovering more
abstract states with a single test case, thus yielding higher gains.

6 Conclusions and Future Work

This paper discusses the synergies between static and dynamic approaches and
proposes a way of quantifying the gain that derives from the synergy of the dif-
ferent approaches, exemplifying it on some popular proposals. The paper makes
some simplifying assumptions that have a limited impact on the generality of
the results presented in this paper. In this concluding section, we discuss the
main assumptions to indicate possible directions for future work.

Different kinds of safety properties. This paper focuses on reachability properties
of programs. Reachability has the desirable feature of being both simple concep-
tually and relevant in practice, and is an important kind of safety property. Safety
properties express the fact that “something bad will not happen”, and their viola-
tion can be detected by observing a finite prefix of infinite violating computations.
A wide range of safety properties are customarily considered in software engineer-
ing, for instance assertions and code contracts (preconditions, postconditions, in-
variants). Focusing on reachability alone may appear somehow reductive. From a
purely theoretical viewpoint, every safety property can be expressed as an equiva-
lent reachability one over an instrumented version of the program under analysis.
As an example, assertions can be encoded as guarded assignments that set a flag
when the assertion is violated. In practice, there exists specialized approaches that
detect violations of a safety specification expressed in a specification language, like
JML [5]. These methods can be studied orthogonally to the state space exploration
techniques which are the main topic of this paper.

Liveness properties. We do not consider liveness properties either. Liveness prop-
erties state that every program computation eventually does “something useful”.