Algorithmic Analysis of Array-Accessing Programs

Date Added: Jun 2009
Format: PDF

For programs whose data variables range over boolean or nite domains, program verification is decidable, and this forms the basis of recent tools for software model checking. In this paper, the authors 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. They show that the reachability problem, while undecidable in general, is Pspace-complete for programs in which the array-accessing for-loops are not nested, decidable for a restricted class of programs with doubly-nested loops.