The Library
On model checking data-independent systems with arrays with whole-array operations
Tools
Tools
Tools
Lazic, Ranko, Newcomb, Tom and Roscoe, A. W. (2004) On model checking data-independent systems with arrays with whole-array operations. University of Warwick. Department of Computer Science. (Department of Computer Science research report). (Unpublished)
|
PDF
WRAP_cs-rr-395.pdf - Other - Requires a PDF viewer. Download (325Kb) | Preview |
Abstract
We consider programs which are data independent with respect to two type variables X and Y, and can in addition use arrays indexed by X and storing values from Y. We are interested in whether a program satisfies its control-state unreachability specification for all non-empty finite instances of X and Y. The decidability of this problem without whole-array operations is a corollary to earlier results. </p><p> We address the possible addition of two whole-array operations: an array reset instruction, which sets every element of an array to a particular value, and an array assignment or copy instruction. For programs with reset, we obtain decidability if there is only one array or if Y is fixed to be the boolean type, and we obtain undecidability otherwise. For programs with array assignment, we show that they are more expressive than programs with reset, which yields undecidability if there are at least three arrays. We also obtain undecidability for two arrays directly.
| Item Type: | Report | ||||
|---|---|---|---|---|---|
| Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | ||||
| Divisions: | Faculty of Science > Computer Science | ||||
| Library of Congress Subject Headings (LCSH): | Machine theory, System theory -- Mathematical models | ||||
| Series Name: | Department of Computer Science research report | ||||
| Publisher: | University of Warwick. Department of Computer Science | ||||
| Official Date: | 2004 | ||||
| Dates: |
|
||||
| Number: | Number 395 | ||||
| Number of Pages: | 17 | ||||
| DOI: | CS-RR-395 | ||||
| Institution: | University of Warwick | ||||
| Theses Department: | Department of Computer Science | ||||
| Status: | Not Peer Reviewed | ||||
| Publication Status: | Unpublished | ||||
| Funder: | Engineering and Physical Sciences Research Council (EPSRC), Intel Corporation, QinetiQ (Firm), United States. Office of Naval Research | ||||
| Grant number: | GR/M32900 (EPSRC) | ||||
| Related URLs: |
Request changes or add full text files to a record
Repository staff actions (login required)
 |
View Item |
Downloads
Downloads per month over past year
