Who is pointing when to whom: on model-checking pointer structures

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.