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

Note that the abstract state space exploration procedure requires to initialize
S A by an arbitrary over-approximation I . In some cases, a monotonic map exists
− − :

T that, applied to a set of concrete states, produce an abstract
over-approximation of it:

P ( S ) →

S ⊆ S − .

− − , when applied to a set of concrete states which
is perfectly described by an abstract value S A , returns such value. We will be
less demanding, and be content when

One would also expect that

− − returns an underapproximation of

S A :

S A − S A .

Any pair of monotonic maps enjoying the above properties forms what is com-
monly known as a Galois connection ,ofwhich

− − is said to be the abstraction

and the concretization maps respectively. A Galois connection satisfies many

properties, among which:

−

− − completely preserves joins, i.e., S∈T S∈T − = − , for all T

- S S ⊆

P ( S ),

− is the smallest abstract value which covers S ,
- S A is the greatest set of states which can be soundly approximated by S A .

- S

The last property is simply a restatement of the fact that S A is the meaning,

or extension, of S A .
Recasting the fixpoint computation into a simpler lattice can solve the

infinity issues. The reachable state space is, in the general case, uncomputable,
but when

T

has finite height, the procedure always converges. When this happens
because the abstract invariance termination check succeeds, the procedure finds a
safe program invariant in

T

that contains the reachable state space, and answers
CORRECT . When the abstract reachability termination check succeeds, nothing
can be said about program correctness, unless A is exact (i.e., all of

T

Post A

,

I A O A

are equal to their concrete counterparts). Correspondingly, the
procedure returns either INCONCLUSIVE or INCORRECT .

,and

Example: Symbolic execution. All the symbolic analyses can be formalized by
means of abstract interpretation as illustrated above. As an example, we discuss
symbolic execution , a well known technique introduced in the seventies [15].
While an ordinary program execution computes program states over concrete
initial values (integers in our example language), symbolic execution summarizes
infinite sets of such computations by computing program states over symbolic
initial values. Symbolic execution produces symbolic states . A symbolic state
maps the program variables to symbolic expressions that describe the current
values of the variables as functions of their initial values. In our example guarded
command language, a symbolic computation step fires simultaneously all the
guarded assignments over an initial symbolic state and cumulates the resulting
symbolic states. Firing a guarded assignment over a symbolic state updates the
mapping of program variables to symbolic expressions to reflect the effect of the