Information Technology Reference
In-Depth Information
The meaning of a lattice element
Σ
∈P
(
P
(
H
)) is, quite simply, the extension
de
=
, where we define the extension of a formula
φ
analogously to our previous definition of extension of an expression:
Σ
Σ
of its translation,
de
=
φ
{
s
∈
S
|
s
|
=
φ
}
.
As an example, let us consider
H
de
=
and
Σ
de
=
{
h
0
,h
1
,h
2
}
{{
h
0
,h
1
}
,
{
h
0
,h
2
}}
.
Then, the meaning of
Σ
is the extension of
h
2
).
A lattice elements can alternatively be seen as a set of bitvectors, where each
position corresponds to a predicate in
H
, and the corresponding bit indicates
the predicate truth value. As an example, the above defined
Σ
can be considered
as the bitvector set
Σ
=(
h
0
∧
h
1
∧¬
h
2
)
∨
(
h
0
∧¬
h
1
∧
{
110
,
101
}
.
ExplorePredicateAbstraction(
p
,
I
,
O
,
H
):
S
H
Σ ∈P
(
P
(
H
))
s.t.
I ⊆{s ∈
S
| s |
=
Σ
}
:= some
O
H
Σ ∈P
(
P
(
H
))
s.t.
{s ∈
S
| s |
=
Σ
}⊆O
:= some
loop:
if
S
H
⊆ O
H
return INCONCLUSIVE
S
H
:=
Post
H
(
p, S
H
)
S
H
⊆ S
H
if
return CORRECT
S
H
∪ S
H
S
H
:=
Fig. 8.
State space exploration by means of predicate abstraction
Figure 8 shows the state space exploration via predicate abstraction. The
lattice of predicate abstraction being finite, the procedure always converges.
Lattice operations are very simple to implement, for instance by means of ordered
binary decision diagrams. The critical part of the procedure is the construction
of Post
H
.Indeed,anoptimalPost
H
exists, namely, the
existential
abstraction
Post
H
:
Post
H
(
p, Σ
)
de
=
σ∈Σ
σ
p
σ
∈P
σ
}
{
(
H
)
|
→
,
where
σ
p
σ
iff Post(
p,
σ
→
σ
∩
∅
.
)
=
p
→
such that
s
p
In other words,
σ
s
.The
existential abstraction is not computable in the general case, but any sound
Post
H
must contain it (i.e., Post
H
(
p, Σ
)
σ
iff exist
s
∈
σ
,s
∈
σ
→
Post
H
(
p, Σ
)) yielding a sound, albeit
less precise, analysis. If we assume the availability of an oracle that can decide the
underlying predicate logic, we can build the existential abstraction, for instance
through symbolic execution:
σ
p
⊆
σ
iff
σ
≡
→
Post
sy
(
p,
{
(id
,
σ
)
}
)
∧
false.
For the sake of simplicity we define the
strongest postcondition predicate trans-
former
sp(
p, φ
)as:
Search WWH ::
Custom Search