Abstraction-Driven Verification of Array Programs - Artificial Intelligence and Symbolic Computation - page 274

municate also ground facts on the signature of and not only the equalities

over shared constants (cf. line 5 of check comb ). The function

PA

purify is such that

purify ( β )=( β 1 ,β 2 ), β is satisfiable iff β 1 ∧ β 2 is, β 1 ( β 2 , resp.) is a conjunction

of literals not containing terms of PA ( ET ,resp.),and α is an arrangement for

β 1 and β 2 (see [11] for a definition).

Notice that the superposition prover plays two roles. First, it implements the
satisfiability procedure for ET . Second, it finds ground instances of the quantified

φ 0 , which are then sent to the decision procedure for PA

sub-formulae in .Notice

that if the calls to the superposition prover returns, then check comb terminates
since there are only finitely many arrangements

α

's (see again [11] for details) and
only finitely many clauses are generated by superposition (given its termination).
So, check fol is terminating whenever the call to check comb returns. Finally, the
algorithm is obviously sound but it is incomplete for an arbitrary ET .

Table 1. Experimental Results on Array Programs

Simplify haRVey

Find (20) 14 20

Selection (14) 12 14

Heap (22) 13 17

3 Experiments: Verification of Array Programs

We have built a prototype version of check fol on top of haRVey 1 [2] by adding an
implementation of check comb and a procedure for the quantifier-free fragment
of

PA

based on the Fourier-Motzkin method (see e.g. [12]). We have used the
Why 2 tool to generate the proof obligations encoding the (total) correctness of
the following programs: Hoare's Find, Selection sort, and Heap sort [5]. Why is
capable of generating proof obligations in the formats of several tools, among
which haRVey and the state-of-the-art theorem prover for program verification,
Simplify [3]. In Table 1, the first column reports the identifier of the algorithm
and the total number of proof obligations encoding its correctness; the second
(third) column gives the number of proof obligations proved by Simplify (our
algorithm, resp.). For Find and Selection sort, Simplify fails to prove about
25% of the proof obligations whereas our system proves them all. For Heap sort,
Simplify proves 13 over 22 formulae whereas our system proves 17. If we add three
lemmas about an inductive predicate recognizing heaps (see [5] for details), then
Simplify proves 16 formulae whereas our system goes to 22. For Find, 19 of the
20 proof obligations are ground after the invocation of top ex at line 1 in Figure
2. On the sole non-ground proof obligation, we have terminated Simplify after
half an hour of work; our system, instead, terminates with the correct answer in
about 10 seconds. For Selection sort and Heap sort, no proof obligation becomes

1 http://www.loria.fr/~ranise/haRVey
2 http://why.lri.fr