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.
|Place of Publication||Enschede|
|Publisher||Centre for Telematics and Information Technology (CTIT)|
|Number of pages||79|
|Publication status||Published - Apr 2003|
|Publisher||University of Twente, Centre for Telematics and Information Technology (CTIT)|
Distefano, D. S., Rensink, A., & Katoen, J. P. (2003). Who is pointing when to whom: on model-checking pointer structures. (CTIT-technical reports; No. 2003-..). Enschede: Centre for Telematics and Information Technology (CTIT).