The theory of arrays, introduced by McCarthy in his seminal paper "Towards 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 have 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 the theories decided by the available procedures. Our approach aims to re-use as much as possible existing techniques so as to ease the implementation of the proposed methods. To this end, we show how to use model-theoretic, rewriting-based theorem proving (i.e., superposition), and techniques developed in the Satisfiability Modulo Theories communities to implement the decision procedures for the various extensions. © 2007 Springer Science+Business Media B.V.

Decision procedures for extensions of the theory of arrays / Ghilardi, S.; Nicolini, E.; Ranise, S.; Zucchelli, D.. - In: ANNALS OF MATHEMATICS AND OF ARTIFICIAL INTELLIGENCE. - ISSN 1012-2443. - 50:3-4(2007), pp. 231-254. [10.1007/s10472-007-9078-x]

Decision procedures for extensions of the theory of arrays

Ranise S.;
2007-01-01

Abstract

The theory of arrays, introduced by McCarthy in his seminal paper "Towards 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 have 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 the theories decided by the available procedures. Our approach aims to re-use as much as possible existing techniques so as to ease the implementation of the proposed methods. To this end, we show how to use model-theoretic, rewriting-based theorem proving (i.e., superposition), and techniques developed in the Satisfiability Modulo Theories communities to implement the decision procedures for the various extensions. © 2007 Springer Science+Business Media B.V.
2007
3-4
Ghilardi, S.; Nicolini, E.; Ranise, S.; Zucchelli, D.
Decision procedures for extensions of the theory of arrays / Ghilardi, S.; Nicolini, E.; Ranise, S.; Zucchelli, D.. - In: ANNALS OF MATHEMATICS AND OF ARTIFICIAL INTELLIGENCE. - ISSN 1012-2443. - 50:3-4(2007), pp. 231-254. [10.1007/s10472-007-9078-x]
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/333004
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 34
  • ???jsp.display-item.citation.isi??? 22
  • OpenAlex ND
social impact