conference paper published yes Rajeev Alur author Pavol Cerny author 4DCBEFFE-F248-11E8-B48F-1D18A9856A87 Scott Weinstein author CSL: Computer Science Logic 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 paper, 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 a potentially 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. Springer2009Coimbra, Portugal eng 10.1007/978-3-642-04027-6_9 577186 - 101 https://research-explorer.ista.ac.at/record/2967 yes Alur, Rajeev, Pavol Cerny, and Scott Weinstein. “Algorithmic Analysis of Array-Accessing Programs,” 5771:86–101. Springer, 2009. <a href="https://doi.org/10.1007/978-3-642-04027-6_9">https://doi.org/10.1007/978-3-642-04027-6_9</a>. Alur, Rajeev, et al. <i>Algorithmic Analysis of Array-Accessing Programs</i>. Vol. 5771, Springer, 2009, pp. 86–101, doi:<a href="https://doi.org/10.1007/978-3-642-04027-6_9">10.1007/978-3-642-04027-6_9</a>. Alur R, Cerny P, Weinstein S. 2009. Algorithmic analysis of array-accessing programs. CSL: Computer Science Logic, LNCS, vol. 5771, 86–101. Alur, R., Cerny, P., &#38; Weinstein, S. (2009). Algorithmic analysis of array-accessing programs (Vol. 5771, pp. 86–101). Presented at the CSL: Computer Science Logic, Coimbra, Portugal: Springer. <a href="https://doi.org/10.1007/978-3-642-04027-6_9">https://doi.org/10.1007/978-3-642-04027-6_9</a> Alur R, Cerny P, Weinstein S. Algorithmic analysis of array-accessing programs. In: Vol 5771. Springer; 2009:86-101. doi:<a href="https://doi.org/10.1007/978-3-642-04027-6_9">10.1007/978-3-642-04027-6_9</a> R. Alur, P. Cerny, S. Weinstein, in:, Springer, 2009, pp. 86–101. R. Alur, P. Cerny, and S. Weinstein, “Algorithmic analysis of array-accessing programs,” presented at the CSL: Computer Science Logic, Coimbra, Portugal, 2009, vol. 5771, pp. 86–101. 44032018-12-11T12:08:40Z2026-07-07T14:01:58Z