Skip to content Skip to navigation
University of Warwick
  • Study
  • |
  • Research
  • |
  • Business
  • |
  • Alumni
  • |
  • News
  • |
  • About

University of Warwick
Publications service & WRAP

Highlight your research

  • WRAP
    • Home
    • Search WRAP
    • Browse by Warwick Author
    • Browse WRAP by Year
    • Browse WRAP by Subject
    • Browse WRAP by Department
    • Browse WRAP by Funder
    • Browse Theses by Department
  • Publications Service
    • Home
    • Search Publications Service
    • Browse by Warwick Author
    • Browse Publications service by Year
    • Browse Publications service by Subject
    • Browse Publications service by Department
    • Browse Publications service by Funder
  • Help & Advice
University of Warwick

The Library

  • Login
  • Admin

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)

[img]
Preview
PDF
WRAP_cs-rr-395.pdf - Other - Requires a PDF viewer.

Download (325Kb) | Preview

Request Changes to record.

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, Engineering and Medicine > 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:
DateEvent
2004Completion
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:
  • Publisher

Request changes or add full text files to a record

Repository staff actions (login required)

View Item View Item

Downloads

Downloads per month over past year

View more statistics

twitter

Email us: wrap@warwick.ac.uk
Contact Details
About Us