# The Library

### On model checking data-independent systems with arrays without reset

Tools

UNSPECIFIED
(2004)
*On model checking data-independent systems with arrays without reset.*
In: 2nd International Workshop on Verification and Computational Logic (VCL 2001), Florence, ITALY, SEP 04, 2001. Published in: THEORY AND PRACTICE OF LOGIC PROGRAMMING, 4
(Part 5-6). pp. 659-693.

**Full text not available from this repository.**

Official URL: http://dx.doi.org/10.1017/S1471068404002054

## Abstract

A system is data-independent with respect to a data type X iff the operations it can perform on values of type X are restricted to just equality testing. The system may also store, input and output values of type X. We study model checking of systems which are data-independent with respect to two distinct type variables X and Y, and may in addition use arrays with indices from X and values from Y. Our main interest is the following parameterised model-checking problem: whether a given program satisfies a given temporal-logic formula for all non-empty finite instances of X and Y. Initially, we consider instead the abstraction where X and Y are infinite and where partial functions with finite domains are used to model arrays. Using a translation to data-independent systems without arrays, we show that the mu-calculus model-checking problem is decidable for these systems. From this result, we can deduce properties of all systems with finite instances of X and Y. We show that there is a procedure for the above parameterised model-checking problem of the universal fragment of the mu-calculus, such that it always terminates but may give false negatives. We also deduce that the parameterised model-checking problem of the universal disjunction-free fragment of the mu-calculus is decidable. Practical motivations for model checking data-independent systems with arrays include verification of memory and cache systems, where X is the type of memory addresses, and Y the type of storable values. As an example we verify a fault-tolerant memory interface over a set of unreliable memories.

Item Type: | Conference Item (UNSPECIFIED) |
---|---|

Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software |

Journal or Publication Title: | THEORY AND PRACTICE OF LOGIC PROGRAMMING |

Publisher: | CAMBRIDGE UNIV PRESS |

ISSN: | 1471-0684 |

Official Date: | September 2004 |

Volume: | 4 |

Number: | Part 5-6 |

Number of Pages: | 35 |

Page Range: | pp. 659-693 |

Identification Number: | 10.1017/S1471068404002054 |

Publication Status: | Published |

Title of Event: | 2nd International Workshop on Verification and Computational Logic (VCL 2001) |

Location of Event: | Florence, ITALY |

Date(s) of Event: | SEP 04, 2001 |

URI: | http://wrap.warwick.ac.uk/id/eprint/7875 |

Data sourced from Thomson Reuters' Web of Knowledge

Request changes or add full text files to a record

### Actions (login required)

View Item |