{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:43Z","timestamp":1760202643682,"version":"3.41.0"},"reference-count":23,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2012,8,1]],"date-time":"2012-08-01T00:00:00Z","timestamp":1343779200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["QUAREM"],"award-info":[{"award-number":["QUAREM"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000144","name":"Division of Computer and Network Systems","doi-asserted-by":"publisher","award":["CNS 0524059"],"award-info":[{"award-number":["CNS 0524059"]}],"id":[{"id":"10.13039\/100000144","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["S11402-N23"],"award-info":[{"award-number":["S11402-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2012,8]]},"abstract":"<jats:p>For programs whose data variables range over Boolean or finite domains, program verification is decidable, and this forms the basis of recent tools for software model checking. In this article, we consider algorithmic verification of programs that use Boolean variables, and in addition, access a single read-only array whose length is potentially unbounded, and whose elements range over an unbounded data domain. We show that the reachability problem, while undecidable in general, is (1) Pspace-complete for programs in which the array-accessing for-loops are not nested, (2) decidable for a restricted class of programs with doubly nested loops. The second result establishes connections to automata and logics defining languages over data words.<\/jats:p>","DOI":"10.1145\/2287718.2287727","type":"journal-article","created":{"date-parts":[[2012,8,28]],"date-time":"2012-08-28T13:09:44Z","timestamp":1346159384000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Algorithmic analysis of array-accessing programs"],"prefix":"10.1145","volume":"13","author":[{"given":"Rajeev","family":"Alur","sequence":"first","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA"}]},{"given":"Pavol","family":"\u010cern\u00fd","sequence":"additional","affiliation":[{"name":"IST Austria, Klosterneuburg, Austria"}]},{"given":"Scott","family":"Weinstein","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA"}]}],"member":"320","published-online":{"date-parts":[[2012,8,28]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_12"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503274"},{"volume-title":"Proceedings of the International Symposium on Mathematical Foundations of Computer Science. 750--761","author":"Bj\u00f6rklund H.","key":"e_1_2_1_3_1","unstructured":"Bj\u00f6rklund , H. and Boja\u0144czyk , M . 2007. Shuffle expressions and words with nested data . In Proceedings of the International Symposium on Mathematical Foundations of Computer Science. 750--761 . Bj\u00f6rklund, H. and Boja\u0144czyk, M. 2007. Shuffle expressions and words with nested data. In Proceedings of the International Symposium on Mathematical Foundations of Computer Science. 750--761."},{"volume-title":"Proceedings of the International Symposium on Foundations of Computation Theory. 88--99","author":"Bj\u00f6rklund H.","key":"e_1_2_1_4_1","unstructured":"Bj\u00f6rklund , H. and Schwentick , T . 2007. On notions of regularity for data languages . In Proceedings of the International Symposium on Foundations of Computation Theory. 88--99 . Bj\u00f6rklund, H. and Schwentick, T. 2007. On notions of regularity for data languages. In Proceedings of the International Symposium on Foundations of Computation Theory. 88--99."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.51"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74240-1_1"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_28"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.31"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1514894.1514924"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/358746.358767"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040333"},{"volume-title":"Proceedings of the International Conference on Computer-Aided Verification. 72--83","author":"Graf S.","key":"e_1_2_1_12_1","unstructured":"Graf , S. and Sa\u00efdi , H . 1997. Construction of abstract state graphs with PVS . In Proceedings of the International Conference on Computer-Aided Verification. 72--83 . Graf, S. and Sa\u00efdi, H. 1997. Construction of abstract state graphs with PVS. In Proceedings of the International Conference on Computer-Aided Verification. 72--83."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181790"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328468"},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Habermehl P. Iosif R. and Vojna\u0159 T. 2008. What else is decidable about integer arrays&quest; In Proceedings of the International Conference on Foundations of Software Science and Computation Structures. 474--489.   Habermehl P. Iosif R. and Vojna\u0159 T. 2008. What else is decidable about integer arrays&quest; In Proceedings of the International Conference on Foundations of Software Science and Computation Structures. 474--489.","DOI":"10.1007\/978-3-540-78499-9_33"},{"volume-title":"Proceedings of the International Conference on Computer-Aided Verification. 526--538","author":"Henzinger T.","key":"e_1_2_1_16_1","unstructured":"Henzinger , T. , Jhala , R. , Majumdar , R. , Necula , G. , Sutre , G. , and Weimer , W . 2002. Temporal-safety proofs for systems code . In Proceedings of the International Conference on Computer-Aided Verification. 526--538 . Henzinger, T., Jhala, R., Majumdar, R., Necula, G., Sutre, G., and Weimer, W. 2002. Temporal-safety proofs for systems code. In Proceedings of the International Conference on Computer-Aided Verification. 526--538."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90242-9"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.4153\/CMB-1961-032-6"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.08.001"},{"volume-title":"Department of Computer Science","author":"Lipton R.","key":"e_1_2_1_20_1","unstructured":"Lipton , R. 1976. The reachability problem requires exponential space. Tech. rep. 62 , Department of Computer Science , Yale University . Lipton, R. 1976. The reachability problem requires exponential space. Tech. rep. 62, Department of Computer Science, Yale University."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.2307\/1970290"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1013560.1013562"},{"key":"e_1_2_1_23_1","unstructured":"Papadimitriou C. 1994.Computational Complexity. Addison-Wesley Publishing Reading MA.  Papadimitriou C. 1994.Computational Complexity. Addison-Wesley Publishing Reading MA."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2287718.2287727","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2287718.2287727","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:49:04Z","timestamp":1750236544000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2287718.2287727"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8]]},"references-count":23,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,8]]}},"alternative-id":["10.1145\/2287718.2287727"],"URL":"https:\/\/doi.org\/10.1145\/2287718.2287727","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2012,8]]},"assertion":[{"value":"2010-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-08-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}