Information Technology Reference
In-Depth Information
example, consider a satisfiability procedure for the union of (the quantifier-free
fragment of) the theory
E
of equality, the quantifier-free fragment of Presburger
arithmetic
PA
,andtheformula
a<b∧
max(
a, b
)=
a ∧∀X, Y.
(
X<Y⇒
max(
X, Y
)=
Y
)
.
(1)
The available procedure will fail to detect the unsatisfiability of (1) since it
does not know how to instantiate the quantified variables. Here, we propose a
mechanism to augment decision procedures to cope with quantifiers.
2
Abstraction-Driven Refutation Theorem Proving
For lack of space, we assume the basic notions of first-order logic [4], the super-
position calculus [8], and the Nelson-Oppen combination schema [7].
Handling Ground Formulae.
Recently, there has been a lot of interest around
theorem proving algorithms to discharge the proof obligations arising in various
verification problems, which are large ground formulae with a complex Boolean
structure to be checked satisfiable modulo a background theory
.Anintegration
of propositional solving (SAT, for short) and satisfiability checking modulo
T
T
has been advocated to eciently discharge these formulae. The
abstract-check-
refine
algorithm underlying such integrations is depicted in Figure 1, where
gfol2prop
(
φ
g
) returns the propositional abstraction of the ground formula
φ
g
(e.g. the abstraction of (
a
=
b ∧ b
=
c
)
⇒ f
(
a
)=
f
(
c
)is(
p ∧ q
)
⇒ r
,
p
is the
abstraction of
a
=
b
,
q
of
b
=
c
,and
r
of
f
(
a
)=
f
(
c
)),
prop2gfol
is its inverse,
and
check assign
is such that
check assign
(
T ,β
)=
unsat
iff
β
is unsatisfiable
modulo
)=
sat
. Many refinements are necessary
to make this schema ecient (see e.g. [6] for details).
T
;otherwise,
check assign
(
T ,β
Handling Non-ground Formulae.
Although the algorithm of Figure 1 has proved
to be very effective for hardware verification problems (see again [6] for ex-
perimental evidence of this), its applicability in program verification is limited
function
check ground
(
φ
g
:
ground formula
)
1
φ
p
←− gfol2prop
(
φ
g
)
2
while
φ
p
=
false
do
3
begin
4
β
p
←−
pick a propositional assignment of
φ
p
ρ←− check assign
(
T , prop2gfol
(
β
p
))
5
6
if
ρ
=
sat
then return
sat
φ
p
←− φ
p
∧¬gfol2prop
(
β
p
)
7
8
end
9
return
unsat
end
Fig. 1.
A refutation-based algorithm for
ground
formulae
Search WWH ::
Custom Search