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]

open access
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
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/47298
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 217626