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

Abstraction-Driven Verification
of Array Programs

David Deharbe 1 , Abdessamad Imine 2 , and Silvio Ranise 2

1 UFRN/DIMAp, Natal, Brazil
[e-mail]
2 LORIA & INRIA-Lorraine, Nancy, France
{ imine,ranise } @loria.fr

Abstract. We describe a refutation-based theorem proving algorithm
capable of checking the satisfiability of non-ground formulae modulo (a
combination of) theories. The key idea is the use of abstraction to drive
the application of ( i ) ground satisfiability checking modulo theories ax-
iomatized by equational clauses, ( ii ) Presburger arithmetic, and ( iii )
quantifier instantiation. A prototype implementation is used to discharge
the proof obligations necessary to show the correctness of some typical
programs manipulating arrays. On these benchmarks, the prototype au-
tomatically discharge more proof obligations than Simplify - the prover
of reference for program checking - thereby confirming the viability of
our approach.

1 Context and Motivation

Satisfiability procedures for equality and theories of standard data-types, such as
arrays, lists, and arithmetic are at the core of most state-of-the-art verification
tools (e.g., DPLL( ) [6] and Simplify [3]). These are required for a wide range

of verification tasks and are fundamental for eciency. Satisfiability problems
have the form

T

T∧φ ,where φ is a Boolean combination of ground literals, T

is a background theory , and the goal is to prove that T∧φ is unsatisfiable. A

satisfiability procedure for a theory T is an algorithm capable of checking whether

T∧φ .

The task of designing, proving correct, and implementing satisfiability pro-
cedures for decidable theories of practical interest is quite di cult. First, most
problems involve more than one theory, so that one needs to combine satisfi-
ability procedures (see e.g. [7]). Second, every satisfiability procedure needs to
be proved correct: a key step is to show that whenever the algorithm reports
“satisfiable,” its final state represents a model of

is satisfiable or not, for any ground formula φ

. Unfortunately, model-
construction arguments can be quite complex (see e.g., [10]).
Although designing and combining decision procedures are necessary and
very important activities to build practically useful reasoning tools, they are
not sucient. In fact, many proof obligations encountered in routine verification
problems require a degree of flexibility which is not provided by actual state-of-
the-art tools. The main problem is that only a tiny portion of such proof obliga-
tions falls exactly into the domain the procedures are designed to solve. As an

T∧φ