{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,12]],"date-time":"2025-02-12T05:13:13Z","timestamp":1739337193828,"version":"3.37.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642040269"},{"type":"electronic","value":"9783642040276"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-04027-6_9","type":"book-chapter","created":{"date-parts":[[2009,9,14]],"date-time":"2009-09-14T17:27:52Z","timestamp":1252949272000},"page":"86-101","source":"Crossref","is-referenced-by-count":5,"title":["Algorithmic Analysis of Array-Accessing Programs"],"prefix":"10.1007","author":[{"given":"Rajeev","family":"Alur","sequence":"first","affiliation":[]},{"given":"Pavol","family":"\u010cern\u00fd","sequence":"additional","affiliation":[]},{"given":"Scott","family":"Weinstein","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","unstructured":"Alur, R., \u010cern\u00fd, P., Weinstein, S.: Algorithmic analysis of array-accessing programs. Technical Report MS-CIS-08-35. University of Pennsylvania (2008)"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-540-30579-8_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"I. Balaban","year":"2005","unstructured":"Balaban, I., Pnueli, A., Zuck, L.D.: Shape analysis by predicate abstraction. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 164\u2013180. Springer, Heidelberg (2005)"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.: The SLAM project: debugging system software via static analysis. In: POPL, pp. 1\u20133 (2002)","DOI":"10.1145\/503272.503274"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"750","DOI":"10.1007\/978-3-540-74456-6_66","volume-title":"Mathematical Foundations of Computer Science 2007","author":"H. Bj\u00f6rklund","year":"2007","unstructured":"Bj\u00f6rklund, H., Boja\u0144czyk, M.: Shuffle expressions and words with nested data. In: Ku\u010dera, L., Ku\u010dera, A. (eds.) MFCS 2007. LNCS, vol.\u00a04708, pp. 750\u2013761. Springer, Heidelberg (2007)"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-540-74240-1_9","volume-title":"Fundamentals of Computation Theory","author":"H. Bj\u00f6rklund","year":"2007","unstructured":"Bj\u00f6rklund, H., Schwentick, T.: On notions of regularity for data languages. In: Csuhaj-Varj\u00fa, E., \u00c9sik, Z. (eds.) FCT 2007. LNCS, vol.\u00a04639, pp. 88\u201399. Springer, Heidelberg (2007)"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Boja\u0144czyk, M., Muscholl, A., Schwentick, T., Segoufin, L., David, C.: Two-variable logic on words with data. In: LICS, pp. 7\u201316 (2006)","DOI":"10.1109\/LICS.2006.51"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-74240-1_1","volume-title":"Fundamentals of Computation Theory","author":"A. Bouajjani","year":"2007","unstructured":"Bouajjani, A., Habermehl, P., Jurski, Y., Sighireanu, M.: Rewriting systems with data. In: Csuhaj-Varj\u00fa, E., \u00c9sik, Z. (eds.) FCT 2007. LNCS, vol.\u00a04639, pp. 1\u201322. Springer, Heidelberg (2007)"},{"key":"9_CR8","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":"9_CR9","doi-asserted-by":"crossref","unstructured":"Demri, S., Lazi\u0107, R.: LTL with the freeze quantifier and register automata. In: LICS, pp. 17\u201326 (2006)","DOI":"10.1109\/LICS.2006.31"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Deutsch, A., Hull, R., Patrizi, F., Vianu, V.: Automatic verification of data-centric business processes. In: ICDT, pp. 252\u2013267 (2009)","DOI":"10.1145\/1514894.1514924"},{"issue":"9","key":"9_CR11","doi-asserted-by":"publisher","first-page":"597","DOI":"10.1145\/358746.358767","volume":"24","author":"J. Gischer","year":"1981","unstructured":"Gischer, J.: Shuffle languages, Petri nets, and context-sensitive grammars. Commun. ACM\u00a024(9), 597\u2013605 (1981)","journal-title":"Commun. ACM"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Gopan, D., Reps, T., Sagiv, M.: A framework for numeric analysis of array operations. In: POPL, pp. 338\u2013350 (2008)","DOI":"10.1145\/1047659.1040333"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: CAV, pp. 72\u201383 (1997)","DOI":"10.1007\/3-540-63166-6_10"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: POPL, pp. 235\u2013246 (2008)","DOI":"10.1145\/1328438.1328468"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/978-3-540-78499-9_33","volume-title":"Foundations of Software Science and Computational Structures","author":"P. Habermehl","year":"2008","unstructured":"Habermehl, P., Iosif, R., Vojnar, T.: What else is decidable about integer arrays? In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol.\u00a04962, pp. 474\u2013489. Springer, Heidelberg (2008)"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/3-540-45657-0_45","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Necula, G.C., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 526\u2013538. Springer, Heidelberg (2002)"},{"issue":"2","key":"9_CR17","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/0304-3975(94)90242-9","volume":"134","author":"M. Kaminski","year":"1994","unstructured":"Kaminski, M., Francez, N.: Finite-memory automata. Theoretical Computer Science\u00a0134(2), 329\u2013363 (1994)","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"9_CR18","first-page":"3","volume":"138","author":"R. Lazi\u0107","year":"2005","unstructured":"Lazi\u0107, R.: Decidability of reachability for polymorphic systems with arrays: A complete classification. ENTCS\u00a0138(3), 3\u201319 (2005)","journal-title":"ENTCS"},{"key":"9_CR19","unstructured":"Lipton, R.: The reachability problem requires exponential space. Technical Report Dept. of Computer Science, Research report 62. Yale University (1976)"},{"key":"9_CR20","doi-asserted-by":"publisher","first-page":"437","DOI":"10.2307\/1970290","volume":"74","author":"M. Minski","year":"1962","unstructured":"Minski, M.: Recursive unsolvability of Post\u2019s problem of \u2019tag\u2019 and other topics in theory of Turing machines. Annals of Mathematics\u00a074, 437\u2013455 (1962)","journal-title":"Annals of Mathematics"},{"issue":"3","key":"9_CR21","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1145\/1013560.1013562","volume":"5","author":"F. Neven","year":"2004","unstructured":"Neven, F., Schwentick, T., Vianu, V.: Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Logic\u00a05(3), 403\u2013435 (2004)","journal-title":"ACM Trans. Comput. Logic"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04027-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,12]],"date-time":"2025-02-12T04:11:58Z","timestamp":1739333518000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04027-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642040269","9783642040276"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04027-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}