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