{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:56:29Z","timestamp":1725558989138},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642142949"},{"type":"electronic","value":"9783642142956"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14295-6_50","type":"book-chapter","created":{"date-parts":[[2010,7,8]],"date-time":"2010-07-08T18:36:09Z","timestamp":1278614169000},"page":"570-584","source":"Crossref","is-referenced-by-count":2,"title":["On Array Theory of Bounded Elements"],"prefix":"10.1007","author":[{"given":"Min","family":"Zhou","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fei","family":"He","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bow-Yaw","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ming","family":"Gu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"50_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1007\/978-3-642-02658-4_15","volume-title":"CAV 2009","author":"M. Bozga","year":"2009","unstructured":"Bozga, M., Habermehl, P., Iosif, R., Kone\u010dn\u00fd, F., Vojnar, T.: Automatic verification of integer array programs. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 157\u2013172. Springer, Heidelberg (2009)"},{"key":"50_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 427\u2013442. Springer, Heidelberg (2005)"},{"key":"50_CR3","unstructured":"B\u00fcchi, J.: Weak second-order arithmetic and finite automata (1959)"},{"key":"50_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1007\/978-3-540-89439-1_39","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P. Habermehl","year":"2008","unstructured":"Habermehl, P., Iosif, R., Vojnar, T.: A logic of singly indexed arrays. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 558\u2013573. Springer, Heidelberg (2008)"},{"key":"50_CR5","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2274706","volume":"56","author":"J.Y. Halpern","year":"1991","unstructured":"Halpern, J.Y.: Presburger arithmetic with unary predicates is \n                    \n                      \n                    \n                    ${\\Pi}_1^1$\n                   complete. Journal of Symbolic Logic\u00a056, 56\u201362 (1991)","journal-title":"Journal of Symbolic Logic"},{"key":"50_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/3-540-60630-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.G. Henriksen","year":"1995","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: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol.\u00a01019, pp. 89\u2013110. Springer, Heidelberg (1995)"},{"key":"50_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/BFb0028022","volume-title":"Computer Science Logic","author":"N. Klarlund","year":"1998","unstructured":"Klarlund, N.: Mona & Fido: The logic-automaton connection in practice. In: Nielsen, M., Thomas, W. (eds.) CSL 1997. LNCS, vol.\u00a01414, pp. 311\u2013326. Springer, Heidelberg (1998)"},{"key":"50_CR8","unstructured":"Klarlund, N., M\u00f8ller, A.: MONA Version 1.4 User Manual. BRICS, Department of Computer Science, Aarhus University, Notes Series NS-01-1 (2001), \n                    \n                      http:\/\/www.brics.dk\/mona\/\n                    \n                    \n                   (revision of BRICS NS-98-3)"},{"key":"50_CR9","unstructured":"Matiyasevich, Y.: Enumerable sets are diophantine. Journal of Sovietic Mathematics, 354\u2013358 (1970)"},{"key":"50_CR10","first-page":"21","volume-title":"IFIP Congress","author":"J. Mccarthy","year":"1962","unstructured":"Mccarthy, J.: Towards a mathematical science of computation. In: IFIP Congress, pp. 21\u201328. North-Holland, Amsterdam (1962)"},{"key":"50_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1007\/3-540-49519-3_4","volume-title":"Formal Methods in Computer-Aided Design","author":"M. M\u00f6ller","year":"1998","unstructured":"M\u00f6ller, M., Rue\u00df, H.: Solving bit-vector equations. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol.\u00a01522, p. 524. Springer, Heidelberg (1998)"},{"key":"50_CR12","unstructured":"Nelson, C.G.: Techniques for program verification. PhD thesis, Stanford University, Stanford, CA, USA (1980)"},{"key":"50_CR13","first-page":"29","volume-title":"LICS \u201901","author":"A. Stump","year":"2001","unstructured":"Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.: A decision procedure for an extensional theory of arrays. In: LICS \u201901, Washington, DC, USA, pp. 29\u201337. IEEE Computer Society Press, Los Alamitos (2001)"},{"issue":"1","key":"50_CR14","doi-asserted-by":"publisher","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. JACM\u00a027(1), 191\u2013205 (1980)","journal-title":"JACM"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14295-6_50","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T15:50:27Z","timestamp":1558281027000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14295-6_50"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642142949","9783642142956"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14295-6_50","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}