On model checking data-independent systems with arrays with whole-array operations
UNSPECIFIED (2005) On model checking data-independent systems with arrays with whole-array operations. In: Symposium on 25 Years of Communicating Sequential Processes, London S Bank Univ, London, ENGLAND, JUL 07-08, 2004. Published in: COMMUNICATING SEQUENTIAL PROCESSES: THE FIRST 25 YEARS, 3525 pp. 275-291.Full text not available from this repository.
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. 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:||Conference Item (UNSPECIFIED)|
|Subjects:||Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software|
|Series Name:||LECTURE NOTES IN COMPUTER SCIENCE|
|Journal or Publication Title:||COMMUNICATING SEQUENTIAL PROCESSES: THE FIRST 25 YEARS|
|Editor:||Abadallah, AE and Jones, CB and Sanders, JW|
|Number of Pages:||17|
|Page Range:||pp. 275-291|
|Title of Event:||Symposium on 25 Years of Communicating Sequential Processes|
|Location of Event:||London S Bank Univ, London, ENGLAND|
|Date(s) of Event:||JUL 07-08, 2004|
Actions (login required)