Array Theory of Bounded Elements and its Applications

Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: A write-based solver for SAT modulo the theory of arrays. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design, pp. 14:1–14:8. IEEE Press, Piscataway (2008) Bozga, M., Habermehl, P., Iosif, R., Konečný, F., Vojnar, T.: Automatic verification of integer array programs. In: Proceedings of the International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 5643, pp. 157–172. Springer Berlin Heidelberg (2009) Bradley, A., Manna, Z., Sipma, H.: What’s decidable about arrays? In: Proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 3855, pp. 427–442. Springer Berlin Heidelberg (2006) Brummayer, R., Biere, A.: Lemmas on demand for the extensional theory of arrays. In: Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning. SMT ’08/BPR ’08, pp. 6–11. ACM (2008) Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. In: Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 5505, pp. 174–177. Springer Berlin Heidelberg (2009) Büchi, J.R.: Weak second-order arithmetic and finite automata. Math. Log. Q. 6(1–6), 66–92 (1960) de Moura, L., Bjorner, N.: Generalized, efficient array decision procedures. In: Proceedings of International Conference on Formal Methods in Computer-Aided Design, pp. 45–52 (2009) Furia, C.A.: What’s decidable about sequences? In: Proceedings of the International Conference on Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 6252, pp. 128–142. Springer Berlin Heidelberg (2010) Ganesh, V., Dill, D.: A decision procedure for bit-vectors and arrays. In: Proceedings of the International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 4590, pp. 519–531. Springer Berlin Heidelberg (2007) Ge, Y., Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Proceedings of the International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 5643, pp. 306–320. Springer Berlin Heidelberg (2009) Ge, Y., Barrett, C., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. In: Proceedings of the International Conference on Automated Deduction. Lecture Notes in Computer Science, vol. 4603, pp. 167–182. Springer Berlin Heidelberg (2007) Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Decision procedures for extensions of the theory of arrays. Ann. Math. Artif. Intell. 50, 231–254 (2007) Goel, A., Krstić, S., Fuchs, A.: Deciding array formulas with frugal axiom instantiation. In: Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning. SMT ’08/BPR ’08, pp. 12–17. ACM, New York (2008) Habermehl, P., Iosif, R., Vojnar, T.: A. logic of singly indexed arrays. In: Proceedings of the International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Lecture Notes in Computer Science, vol. 5330, pp. 558–573. Springer, Berlin, Heidelberg (2008) Halpern, J.Y. (1991) Presburger arithmetic with unary predicates is \({\Pi}_1^1\) complete. J. Symb. Log. 56, 637–642 Henriksen, J.G., Jensen, O.J., Jørgensen, M.E., Klarlund, N., Paige, R., Rauhe, T., Sandholm, A.B.: Mona: Monadic second-order logic in practice. In: Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 1019. Springer (1995) Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969) Kapur, D., Zarba, C.: A reduction approach to decision procedures. Tech. rep. (2005) Klarlund, N.: Mona & fido: the logic-automaton connection in practice. In: Conference on Computer Science Logic. Lecture Notes in Computer Science, vol. 1414, pp. 311–326. Springer (1997) Klarlund, N., Møller, A.: MONA Version 1.4 User Manual. BRICS. Department of Computer Science, Aarhus University, notes Series NS-01-1. Revision of BRICS NS-98-3. Available from http://www.brics.dk/mona/ (2001) Matiyasevich, Y.: Enumerable sets are diophantine. Dokl. Akad. Nauk SSSR 191(2), 279–282 (1970) McCarthy, J.: Towards a mathematical science of computation. In: IFIP (International Federation for Information Processing), pp. 21–28 . Congress, North-Holland (1962) Möller, M., Rueß, H.: Solving bit-vector equations. In: Proceedings of International Conference on Formal Methods in Computer-Aided Design, pp. 524–524. Springer (1998) Moura, L., Bjrner, N.: Efficient E-Matching for smt solvers. In: Proceedings of International Conference on Automated Deduction. Lecture Notes in Computer Science, vol. 4603, pp. 183–198. Springer Berlin Heidelberg (2007) Nelson, C.G.: Techniques for program verification. PhD. thesis, Stanford University, Stanford (1980) Stump, A., Barrett, C., Dill, D., Levitt, J.: A decision procedure for an extensional theory of arrays. In: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, pp. 29–37. IEEE Computer Society, Washington (2001) Suzuki, N., Jefferson, D.: Verification decidability of presburger array programs. J. ACM 27(1), 191–205 (1980) Wintersteiger, C., Hamadi, Y., de Moura, L.: Efficiently solving quantified bit-vector formulas. In: Proceedings of International Conference on Formal Methods in Computer-Aided Design, pp. 239–246 (2010) Zhou, M., He, F., Wang, B., Gu, M.: On array theory of bounded elements. In: Proceedings of International Conference on Computer Aided Verification, pp. 570–584. Springer (2010)