Decision procedures for extensions of the theory of arrays

The theory of arrays, introduced by McCarthy in his seminal paper “Toward a mathematical science of computation”, is central to Computer Science. Unfortunately, the theory alone is not sufficient for many important verification applications such as program analysis. Motivated by this observation, we study extensions of the theory of arrays whose satisfiability problem (i.e. checking the satisfiability of conjunctions of ground literals) is decidable. In particular, we consider extensions where the indexes of arrays has the algebraic structure of Presburger Arithmetic and the theory of arrays is augmented with axioms characterizing additional symbols such as dimension, sortedness, or the domain of definition of arrays. We provide methods for integrating available decision procedures for the theory of arrays and Presburger Arithmetic with automatic instantiation strategies which allow us to reduce the satisfiability problem for the extension of the theory of arrays to that of t...

• Type: Journal
• Year: 2007
• Where: AMAI
• Authors: Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli
• Keywords: AMAI 2007, Artificial Intelligence, Presburger Arithmetic, Satisfiability Problem, Theory