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

practice, but that allows us to abstract away from issues that are not relevant
to our tractation.
We now introduce some terminology about the relevant properties of verifi-
cation techniques. We say that a technique is complete w.r.t. correct (incorrect)
programs if, whenever a program is correct (incorrect) w.r.t. an arbitrary reacha-
bility problem, the technique answers CORRECT ( INCORRECT ). From the undecid-
ability of the reachability problem follows that every verification technique has
some degree of incompleteness either w.r.t. correctness or incorrectness. In the
worstcaseatechniquemaybe void w.r.t. correct (incorrect) programs i.e., fails
in producing any CORRECT ( INCORRECT ) answer. We will say that a technique is
more complete than another one whenever the former converges to a conclusive
answer on more inputs than the latter (we may refine the statement by saying
that the technique is more complete w.r.t. correctness, incorrectness or both).
When a technique does not produce a conclusive answer, i.e. either CORRECT or
INCORRECT , it may either converge to INCONCLUSIVE or fail to converge. The two
situations are not, of course, equivalent in practice since a diverging computa-
tion cannot be in general distinguished by a human from a very long converging
computation. We say that a technique converges more than another one when-
ever the former converges (albeit not necessarily to a conclusive answer) on more
inputs than the latter. Finally, we say that a technique is more precise than an-
other one whenever the former is more complete and converges more than the
latter.

3 Exploring the Space of Program Executions

This section introduces and classifies the basic analysis and testing techniques
that are used and combined to prove software properties. Here we propose a tax-
onomy that helps us comparing the various approaches with respect to complete-
ness and convergence. This, in turns, motivates the combination patterns arising
between basic techniques, which is investigated in the next section. We propose
the taxonomy focusing on three categories of basic explorative techniques that
are commonly exploited in combinations of static and dynamic approaches: test-
ing, symbolic execution, and predicate abstraction.

3.1 Full Exhaustive State Space Exploration

A state s e is reachable from some initial state s 0 if there exists at least one finite
sequence of computation steps s 0 p → s 1 p → ... p

→ s e . Thus, an intuitively simple
way to investigate a set of reachable states is to look for such finite computations.
On the above rationale, techniques based on state space exploration unroll the
reachable program state space at increasing (but finite) depth, through real or
simulated program execution. The process is iterated until either an error state is
found, in which case the program is rejected, or all the reachable program states
have been explored, in which case the program is accepted. Testing, explicit-state
or symbolic model checking, and symbolic execution are different declinations of
this paradigms.