---
res:
  bibo_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 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.@eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Rajeev
      foaf_name: Alur, Rajeev
      foaf_surname: Alur
  - foaf_Person:
      foaf_givenName: Pavol
      foaf_name: Cerny, Pavol
      foaf_surname: Cerny
      foaf_workInfoHomepage: http://www.librecat.org/personId=4DCBEFFE-F248-11E8-B48F-1D18A9856A87
  - foaf_Person:
      foaf_givenName: Scott
      foaf_name: Weinstein, Scott
      foaf_surname: Weinstein
  bibo_doi: 10.1007/978-3-642-04027-6_9
  bibo_volume: 5771
  dct_date: 2009^xs_gYear
  dct_language: eng
  dct_publisher: Springer@
  dct_title: Algorithmic analysis of array-accessing programs@
...