caa a22 4500 463187091 CHVBK 20180406164857.0 cr unu---uuuuu 170326e20070801xx s 000 0 eng 10.1007/s10472-007-9078-x doi (NATIONALLICENCE)springer-10.1007/s10472-007-9078-x Decision procedures for extensions of the theory of arrays [Elektronische Daten] [Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli] 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. Springer Science+Business Media B.V., 2007 Constraint satisfiability problems nationallicence Decision procedures nationallicence Combination methods nationallicence Instantiation strategies nationallicence Theory of arrays with extensionality nationallicence Presburger arithmetic nationallicence Ghilardi Silvio Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, Milan, Italy aut Nicolini Enrica LORIA & INRIA-Lorraine, Nancy Cedex, France aut Ranise Silvio LORIA & INRIA-Lorraine, Nancy Cedex, France aut Zucchelli Daniele Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, Milan, Italy aut Annals of Mathematics and Artificial Intelligence Springer Netherlands 50/3-4(2007-08-01), 231-254 1012-2443 50:3-4<231 2007 50 10472 https://doi.org/10.1007/s10472-007-9078-x text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s10472-007-9078-x text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Ghilardi Silvio Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, Milan, Italy aut NATIONALLICENCE 700 1- Nicolini Enrica LORIA & INRIA-Lorraine, Nancy Cedex, France aut NATIONALLICENCE 700 1- Ranise Silvio LORIA & INRIA-Lorraine, Nancy Cedex, France aut NATIONALLICENCE 700 1- Zucchelli Daniele Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, Milan, Italy aut NATIONALLICENCE 773 0- Annals of Mathematics and Artificial Intelligence Springer Netherlands 50/3-4(2007-08-01), 231-254 1012-2443 50:3-4<231 2007 50 10472 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer