Who is pointing when to whom?

D.S. Distefano, Kamal Lodaya (Editor), Joost P. Katoen, Meena Mahajan (Editor), Arend Rensink

    Research output: Contribution to conferencePaperpeer-review

    1 Downloads (Pure)

    Abstract

    This paper introduces an extension of linear temporal logic that allows to express properties about systems that are composed of entities (like objects) that can refer to each other via pointers. Our logic is focused on specifying properties about the dynamic evolution (such as creation, adaptation, and removal) of such pointer structures. The semantics is based on automata on infinite words, extended with appropriate means to model evolving pointer structures in an abstract manner. A tableau-based model-checking algorithm is proposed to automatically verify these automata against formulae in our logic.
    Original languageUndefined
    Pages250-262
    Number of pages13
    DOIs
    Publication statusPublished - 2004
    Event24th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2004 - Chennai, India
    Duration: 16 Dec 200418 Dec 2004
    Conference number: 24

    Workshop

    Workshop24th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2004
    Abbreviated titleFSTTCS
    Country/TerritoryIndia
    CityChennai
    Period16/12/0418/12/04

    Keywords

    • FMT-OO: VERIFICATION OF OBJECT-BASED SYSTEMS
    • IR-63331
    • EWI-6546
    • FMT-MC: MODEL CHECKING

    Cite this