---
_id: '4403'
abstract:
- lang: eng
  text: 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.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Rajeev
  full_name: Alur, Rajeev
  last_name: Alur
- first_name: Pavol
  full_name: Cerny, Pavol
  id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
  last_name: Cerny
- first_name: Scott
  full_name: Weinstein, Scott
  last_name: Weinstein
citation:
  ama: '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>'
  apa: '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>'
  chicago: 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>.
  ieee: '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.'
  ista: 'Alur R, Cerny P, Weinstein S. 2009. Algorithmic analysis of array-accessing
    programs. CSL: Computer Science Logic, LNCS, vol. 5771, 86–101.'
  mla: 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>.
  short: R. Alur, P. Cerny, S. Weinstein, in:, Springer, 2009, pp. 86–101.
conference:
  end_date: 2009-09-11
  location: Coimbra, Portugal
  name: 'CSL: Computer Science Logic'
  start_date: 2009-09-07
date_created: 2018-12-11T12:08:40Z
date_published: 2009-09-01T00:00:00Z
date_updated: 2025-09-30T08:04:32Z
day: '01'
doi: 10.1007/978-3-642-04027-6_9
extern: '1'
intvolume: '      5771'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://repository.upenn.edu/cis_reports/894/
month: '09'
oa: 1
oa_version: Submitted Version
page: 86 - 101
publication_status: published
publisher: Springer
publist_id: '1056'
quality_controlled: '1'
related_material:
  record:
  - id: '2967'
    relation: later_version
    status: public
status: public
title: Algorithmic analysis of array-accessing programs
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 5771
year: '2009'
...