{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:33:08Z","timestamp":1773192788432,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540311393","type":"print"},{"value":"9783540316220","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11609773_28","type":"book-chapter","created":{"date-parts":[[2005,12,12]],"date-time":"2005-12-12T02:28:57Z","timestamp":1134354537000},"page":"427-442","source":"Crossref","is-referenced-by-count":164,"title":["What\u2019s Decidable About Arrays?"],"prefix":"10.1007","author":[{"given":"Aaron R.","family":"Bradley","sequence":"first","affiliation":[]},{"given":"Zohar","family":"Manna","sequence":"additional","affiliation":[]},{"given":"Henny B.","family":"Sipma","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"28_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/3-540-44802-0_36","volume-title":"Computer Science Logic","author":"A. Armando","year":"2001","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: Uniform derivation of decision procedures by superposition. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, p. 513. Springer, Heidelberg (2001)"},{"key":"28_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2004","unstructured":"Barrett, C., Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"key":"28_CR3","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: Polyranking for polynomial loops. In: submission, available at, \n                  \n                    http:\/\/theory.stanford.edu\/~arbrad"},{"key":"28_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Heidelberg (1995)"},{"key":"28_CR5","unstructured":"McCarthy, J.: Towards a mathematical science of computation. In: IFIP Congress 1962 (1962)"},{"key":"28_CR6","volume-title":"Theory of Linear and Integer Programming","author":"A. Schrijver","year":"1986","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Chichester (1986)"},{"key":"28_CR7","unstructured":"Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for an extensional theory of arrays. In: Logic in Computer Science (LICS) (2001)"},{"key":"28_CR8","doi-asserted-by":"publisher","first-page":"1","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\u00a027, 1 (1980)","journal-title":"J. ACM"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11609773_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T03:07:04Z","timestamp":1619492824000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11609773_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540311393","9783540316220"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/11609773_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}