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

Table 1. Features of the basic techniques

Technique Symbolic Abstract Depth

bounded

Width
bounded

non Mono-
tonic

No − Testing No No Yes Yes

No −

Exhaustive testing No No No Yes

Yes − Yes − Yes − Symbolic execution Yes No

Abstract reachability Yes Yes No No No

No − Model checking Both No No No

Bounded model checking Yes No Yes No No

Legend:
Yes/No: Yes/No by definition, Yes − /No − : Yes/No in most cases, Both: Either ways

Symbolic execution. State space exploration via practical symbolic execution
approaches is typically non-monotonic (conveniently since detection of symbolic
loops is hard, and sets of symbolic states are usually represented in an extensional
fashion), depth-bounded (to avoid divergence) and in some cases width-bounded
(to reduce the exploration scope).

Abstract reachability. State space exploration via predicate abstraction is both
symbolic and abstract. The techniques take advantage of the finite size of the ab-
stract state space and the loss in precision by abstraction to explore the abstract
state space in full and monotonically.

Model checking. Model checking is a family of techniques that validate a system
against a specification of some program property, typically expressed in temporal
logic, and produce a counterexample computation if the system violates the
property. From the reachability viewpoint, a model checking procedure explores
the program state space fully and exhaustively, either symbolically or explicitly,
and is typically width-unbounded, depth-unbounded and monotonic. Bounded
model checking is a form of depth-bounded symbolic exploration for finite-state
systems. It starts from a specification of the system Post in propositional logic,
“unrolls” it up to some finite depth, joins it with clauses establishing that the
first state is initial and the last state is an error state, and uses a SAT solver
to decide the satisfiability of the resulting formula. In the positive case, a SAT
solver may produce a satisfying assignment, which can be interpreted as a finite
computation leading to an error state.

4 Combining Techniques by Synergies

Testing and formal analysis techniques trade the precision of state space ex-
ploration against tractability and speed by means of different approximation
strategies that we discussed in the previous section. Approximation criteria typ-
ically yield poor results except for very narrow classes of inputs. For this reason,