Algorithmic analysis of array-accessing programs

R. Alur, P. Cerny, S. Weinstein, ACM Transactions on Computational Logic (TOCL) 13 (2012).

Download
No fulltext has been uploaded. References only!

Journal Article | Published | English
Author
Alur, Rajeev; Cerny, PavolIST Austria; Weinstein, Scott
Department
Abstract
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.
Publishing Year
Date Published
2012-08-01
Journal Title
ACM Transactions on Computational Logic (TOCL)
Acknowledgement
This research was supported in part by the NSF Cybertrust award CNS 0524059, by the European Research Council (ERC) Advanced Investigator Grant QUAREM, and by the Austrian Science Fund (FWF) project S11402-N23.
Volume
13
Issue
3
Article Number
27
IST-REx-ID

Cite this

Alur R, Cerny P, Weinstein S. Algorithmic analysis of array-accessing programs. ACM Transactions on Computational Logic (TOCL). 2012;13(3). doi:10.1145/2287718.2287727
Alur, R., Cerny, P., & Weinstein, S. (2012). Algorithmic analysis of array-accessing programs. ACM Transactions on Computational Logic (TOCL), 13(3). https://doi.org/10.1145/2287718.2287727
Alur, Rajeev, Pavol Cerny, and Scott Weinstein. “Algorithmic Analysis of Array-Accessing Programs.” ACM Transactions on Computational Logic (TOCL) 13, no. 3 (2012). https://doi.org/10.1145/2287718.2287727.
R. Alur, P. Cerny, and S. Weinstein, “Algorithmic analysis of array-accessing programs,” ACM Transactions on Computational Logic (TOCL), vol. 13, no. 3, 2012.
Alur R, Cerny P, Weinstein S. 2012. Algorithmic analysis of array-accessing programs. ACM Transactions on Computational Logic (TOCL). 13(3), 27.
Alur, Rajeev, et al. “Algorithmic Analysis of Array-Accessing Programs.” ACM Transactions on Computational Logic (TOCL), vol. 13, no. 3, 27, ACM, 2012, doi:10.1145/2287718.2287727.
Material in IST:
Earlier Version

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar