## What's Decidable About Arrays?

*Aaron R. Bradley,
Zohar Manna,
Henny B. Sipma.
*
Motivated by applications to program verification, we study a decision
procedure for satisfiability in an expressive fragment of a theory of
arrays, which is parameterized by the theories of the array elements.
The decision procedure reduces satisfiability of a formula of the
fragment to satisfiability of an equisatisfiable quantifier-free
formula in the combined theory of equality with uninterpreted
functions (EUF), Presburger arithmetic, and the element theories.
This fragment allows a constrained use of universal quantification, so
that one quantifier alternation is allowed, with some syntactic
restrictions. It allows expressing, for example, that an assertion
holds for all elements in a given index range, that two arrays are
equal in a given range, or that an array is sorted. We demonstrate
its expressiveness through applications to verification of sorting
algorithms and parameterized systems. We also prove that
satisfiability is undecidable for several natural extensions to the
fragment. Finally, we describe our implementation in the \pvc\
verification system.

In *Proc.of Verification, Model Checking and Abstract
Interpretation (VMCAI'06)*, LNCS 3855,
Springer Verlag, 2006, pp 427-442.

BibTex,
Postscript,
PDF.
© 2006, Springer Verlag.

© Henny Sipma /
sipma@cs.stanford.edu
Last modified: April 7 14:40:50 PDT 2005