Back to University of Twente portal
Who is pointing When to Whom: On Model-Checking Pointer Structures
Distefano, Dino and Rensink, Arend and Katoen, Joost-Pieter (2003) Who is pointing When to Whom: On Model-Checking Pointer Structures. [Report]
![[img]](http://doc.utwente.nl/style/images/fileicons/application_pdf.png)
| PDF 728Kb |
| Abstract: | This paper introduces a new model to reason about systems composed by entities that can refer to each other via pointers, such as objects in an object-based system. The model, based on History-Dependent Automata, treats particular cases of unboundedness by a special layered mechanism of abstraction. As an application, in this paper the model is used to dene the semantics of a simple language dealing with dynamic allocation and deallocation of entities and pointers. Furthermore, the paper presents a temporal logic that allows to express properties for such systems and that is particularly focussed on the way entities refer to each other. Finally, a sound (but not complete) model checking algorithm for the logic is presented. |
| Item Type: | Report |
| Copyright: | © 2003 CTIT |
| Faculty: | Electrical Engineering, Mathematics and Computer Science (EEMCS) |
| Research Group: | |
| Link to this item: | http://purl.utwente.nl/publications/47298 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page
Metis ID: 217626