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.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: On a rewriting approach to satisfiability procedures: extension, combination of theories and an experimental appraisal. In: Proceedings of the 5th International Workshop on Frontiers of Combining Systems (FroCoS’05). LNCS, vol. 3717, pp. 65–80. Springer (2005)
Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Inf. Comput. 183(2), 140–164 (2003)
Bjørner, N., Stickel, M.E., Uribe, T.E.: A practical integration of first-order reasoning and decision procedures. In: Proceedings of the 14th International Conference on Automated Deduction (CADE’97). LNCS, vol. 1249, pp. 101–115. Springer (1997)
Bonacina, M.P., Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures. In: Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR’06). LNCS, vol. 4130, pp. 513–527. Springer (2006)
Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Ranise, S., van Rossum, P., Sebastiani, R.: Efficient theory combination via boolean search. Inf. Comput. 204(10), 1493–1525 (2006)
Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’06). LNCS, vol. 3855, pp. 427–442. Springer (2006)
Brodnik, A., Carlsson, S., Demaine, E.D., Munro, J.I., Sedgewick, R.: Resizable arrays in optimal time and space. In: Proceedings of 6th International Workshop on Algorithms and Data Structures (WADS’99). LNCS, vol. 1663, pp. 37–48. Springer (1999)
Déharbe, D., Ranise, S.: Light-weight theorem proving for debugging and verifying units of code. In: Proceedings of the 1st International Conference on Software Engineering and Formal Methods (SEFM’03), pp. 220–228. IEEE Computer Society (2003)
Downey, P.J., Sethi, R.: Assignment commands with array references. J. ACM 25(4), 652–666 (1978)
Enderton, H.B.: A Mathematical Introduction to Logic. Academic, New York (1972)
Gallier, J.H.: Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row (1986)
Ganzinger, H., Korovin, K.: Integrating equational reasoning in instantiation-based theorem proving. In: Proceedings of the 18th International Workshop on Computer Science in Logic (CSL’04). LNCS, vol. 3210, pp. 71–84. Springer (2004)
Ghilardi, S.: Model-theoretic methods in combined constraint satisfiability. J. Autom. Reason. 33(3–4), 221–249 (2004)
Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Deciding extension of the theory of arrays by integrating decision procedures and instantiation strategies. Rapporto Interno DSI 309-06, Università degli Studi di Milano, Milano (Italy) (2006) Available at http://homes.dsi.unimi.it/~zucchell/publications/techreport/GhiNiRaZu-RI309-06.pdf
Jaffar, J.: Presburger arithmetic with array segments. Inf. Process. Lett. 12(2), 79–82 (1981)
Mateti, P.: A decision procedure for the correctness of a class of programs. J. ACM 28(2), 215–232 (1981)
McCarthy, J.: Towards a mathematical theory of computation. In: Proceedings of IFIP Congress, pp. 21–28 (1962)
McPeak, S., Necula, G.: Data structures specification via local equality axioms. In: Proceedings of the 17th International Conference on Computer Aided Verification (CAV’05). LNCS, vol. 3576, pp. 476–490. Springer (2005)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979)
Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, chapter 7, pp. 371–443. Elsevier Science (2001)
Reynolds, J.C.: Reasoning about arrays. Commun. ACM 22(5), 290–299 (1979)
Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS’02), pp. 55–74. IEEE Computer Society (2002)
Rusinowitch, M.: Démonstration Automatique (Techniques de réécriture). InterEditions (1989)
Schrijver, A.: Theory of Linear and Integer Programming. Wiley (1986)
Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.: A decision procedure for an extensional theory of arrays. In: Proceedings of the 16th IEEE Symposium on Logic in Computer Science (LICS’01). pp. 29–37. IEEE Computer Society (2001)
Suzuki, N., Jefferson, D.R.: Verification decidability of Presburger array programs. J. ACM 27(1), 191–205 (1980)
van Dalen, D.: Logic and Structure, 2nd edn. Springer (1989)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Ghilardi, S., Nicolini, E., Ranise, S. et al. Decision procedures for extensions of the theory of arrays. Ann Math Artif Intell 50, 231–254 (2007). https://doi.org/10.1007/s10472-007-9078-x
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10472-007-9078-x
Keywords
- Constraint satisfiability problems
- Decision procedures
- Combination methods
- Instantiation strategies
- Theory of arrays with extensionality
- Presburger arithmetic