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

    Research output: Book/ReportReportProfessional

    21 Downloads (Pure)


    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.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages79
    Publication statusPublished - Apr 2003

    Publication series

    NameCTIT-technical reports
    PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)


    • EWI-5836
    • METIS-217626
    • IR-47298

    Cite this