{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,24]],"date-time":"2023-01-24T13:30:57Z","timestamp":1674567057081},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2013,9,24]],"date-time":"2013-09-24T00:00:00Z","timestamp":1379980800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2014,4]]},"DOI":"10.1007\/s10817-013-9293-6","type":"journal-article","created":{"date-parts":[[2013,9,23]],"date-time":"2013-09-23T00:54:56Z","timestamp":1379897696000},"page":"379-405","source":"Crossref","is-referenced-by-count":7,"title":["Array Theory of Bounded Elements and its Applications"],"prefix":"10.1007","volume":"52","author":[{"given":"Min","family":"Zhou","sequence":"first","affiliation":[]},{"given":"Fei","family":"He","sequence":"additional","affiliation":[]},{"given":"Bow-Yaw","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Ming","family":"Gu","sequence":"additional","affiliation":[]},{"given":"Jiaguang","family":"Sun","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,9,24]]},"reference":[{"key":"9293_CR1","doi-asserted-by":"crossref","unstructured":"Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-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\u201314:8. IEEE Press, Piscataway (2008)","DOI":"10.1109\/FMCAD.2008.ECP.18"},{"key":"9293_CR2","doi-asserted-by":"crossref","unstructured":"Bozga, M., Habermehl, P., Iosif, R., Kone\u010dn\u00fd, 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\u2013172. Springer Berlin Heidelberg (2009)","DOI":"10.1007\/978-3-642-02658-4_15"},{"key":"9293_CR3","doi-asserted-by":"crossref","unstructured":"Bradley, A., Manna, Z., Sipma, H.: What\u2019s 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\u2013442. Springer Berlin Heidelberg (2006)","DOI":"10.1007\/11609773_28"},{"key":"9293_CR4","doi-asserted-by":"crossref","unstructured":"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 \u201908\/BPR \u201908, pp. 6\u201311. ACM (2008)","DOI":"10.1145\/1512464.1512467"},{"key":"9293_CR5","doi-asserted-by":"crossref","unstructured":"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\u2013177. Springer Berlin Heidelberg (2009)","DOI":"10.1007\/978-3-642-00768-2_16"},{"issue":"1\u20136","key":"9293_CR6","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1002\/malq.19600060105","volume":"6","author":"JR B\u00fcchi","year":"1960","unstructured":"B\u00fcchi, J.R.: Weak second-order arithmetic and finite automata. Math. Log. Q. 6(1\u20136), 66\u201392 (1960)","journal-title":"Math. Log. Q."},{"key":"9293_CR7","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bjorner, N.: Generalized, efficient array decision procedures. In: Proceedings of International Conference on Formal Methods in Computer-Aided Design, pp. 45\u201352 (2009)","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"9293_CR8","doi-asserted-by":"crossref","unstructured":"Furia, C.A.: What\u2019s 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\u2013142. Springer Berlin Heidelberg (2010)","DOI":"10.1007\/978-3-642-15643-4_11"},{"key":"9293_CR9","doi-asserted-by":"crossref","unstructured":"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\u2013531. Springer Berlin Heidelberg (2007)","DOI":"10.1007\/978-3-540-73368-3_52"},{"key":"9293_CR10","doi-asserted-by":"crossref","unstructured":"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\u2013320. Springer Berlin Heidelberg (2009)","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"9293_CR11","doi-asserted-by":"crossref","unstructured":"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\u2013182. Springer Berlin Heidelberg (2007)","DOI":"10.1007\/978-3-540-73595-3_12"},{"key":"9293_CR12","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1007\/s10472-007-9078-x","volume":"50","author":"S Ghilardi","year":"2007","unstructured":"Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Decision procedures for extensions of the theory of arrays. Ann. Math. Artif. Intell. 50, 231\u2013254 (2007)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9293_CR13","doi-asserted-by":"crossref","unstructured":"Goel, A., Krsti\u0107, 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 \u201908\/BPR \u201908, pp. 12\u201317. ACM, New York (2008)","DOI":"10.1145\/1512464.1512468"},{"key":"9293_CR14","doi-asserted-by":"crossref","unstructured":"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\u2013573. Springer, Berlin, Heidelberg (2008)","DOI":"10.1007\/978-3-540-89439-1_39"},{"key":"9293_CR15","doi-asserted-by":"crossref","first-page":"637","DOI":"10.2307\/2274706","volume":"56","author":"JY Halpern","year":"1991","unstructured":"Halpern, J.Y. (1991) Presburger arithmetic with unary predicates is ${\\Pi}_1^1$ complete. J. Symb. Log. 56, 637\u2013642","journal-title":"J. Symb. Log."},{"key":"9293_CR16","doi-asserted-by":"crossref","unstructured":"Henriksen, J.G., Jensen, O.J., J\u00f8rgensen, 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)","DOI":"10.1007\/3-540-60630-0_5"},{"issue":"10","key":"9293_CR17","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"9293_CR18","unstructured":"Kapur, D., Zarba, C.: A reduction approach to decision procedures. Tech. rep. (2005)"},{"key":"9293_CR19","doi-asserted-by":"crossref","unstructured":"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\u2013326. Springer (1997)","DOI":"10.1007\/BFb0028022"},{"key":"9293_CR20","unstructured":"Klarlund, N., M\u00f8ller, 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)"},{"issue":"2","key":"9293_CR21","first-page":"279","volume":"191","author":"Y Matiyasevich","year":"1970","unstructured":"Matiyasevich, Y.: Enumerable sets are diophantine. Dokl. Akad. Nauk SSSR 191(2), 279\u2013282 (1970)","journal-title":"Dokl. Akad. Nauk SSSR"},{"key":"9293_CR22","first-page":"21","volume-title":"IFIP (International Federation for Information Processing)","author":"J McCarthy","year":"1962","unstructured":"McCarthy, J.: Towards a mathematical science of computation. In: IFIP (International Federation for Information Processing), pp. 21\u201328 . Congress, North-Holland (1962)"},{"key":"9293_CR23","doi-asserted-by":"crossref","unstructured":"M\u00f6ller, M., Rue\u00df, H.: Solving bit-vector equations. In: Proceedings of International Conference on Formal Methods in Computer-Aided Design, pp. 524\u2013524. Springer (1998)","DOI":"10.1007\/3-540-49519-3_4"},{"key":"9293_CR24","doi-asserted-by":"crossref","unstructured":"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\u2013198. Springer Berlin Heidelberg (2007)","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"9293_CR25","volume-title":"Techniques for program verification","author":"CG Nelson","year":"1980","unstructured":"Nelson, C.G.: Techniques for program verification. PhD. thesis, Stanford University, Stanford (1980)"},{"key":"9293_CR26","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1109\/LICS.2001.932480","volume-title":"Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science","author":"A Stump","year":"2001","unstructured":"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\u201337. IEEE Computer Society, Washington (2001)"},{"issue":"1","key":"9293_CR27","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1145\/322169.322185","volume":"27","author":"N Suzuki","year":"1980","unstructured":"Suzuki, N., Jefferson, D.: Verification decidability of presburger array programs. J. ACM 27(1), 191\u2013205 (1980)","journal-title":"J. ACM"},{"key":"9293_CR28","unstructured":"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\u2013246 (2010)"},{"key":"9293_CR29","doi-asserted-by":"crossref","unstructured":"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\u2013584. Springer (2010)","DOI":"10.1007\/978-3-642-14295-6_50"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9293-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-013-9293-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9293-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,24]],"date-time":"2019-07-24T11:45:14Z","timestamp":1563968714000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-013-9293-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9,24]]},"references-count":29,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,4]]}},"alternative-id":["9293"],"URL":"https:\/\/doi.org\/10.1007\/s10817-013-9293-6","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,9,24]]}}}
