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