Abstract Graph Transformation

Arend Rensink, D.S. Distefano

    Research output: Book/ReportReportProfessional

    31 Downloads (Pure)

    Abstract

    Graphs may be used as representations of system states in operational semantics and model checking; in the latter context, they are being investigated as an alternative to bit vectors. The corresponding transitions are obtained as derivations from graph production rules. In this paper we propose an abstraction technique in this framework: the state graphs are contracted by collecting nodes that are sufficiently similar (resulting in smaller states and a finite state space) and the application of the graph production rules is lifted to this abstract level. Since graph abstractions and rule applications can all be computed completely automatically, we believe that this can be the core of a practically feasible technique for software model checking.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages25
    Publication statusPublished - Jan 2005

    Publication series

    NameCTIT Technical Report Series
    No.05-04
    ISSN (Print)1381-3625

    Keywords

    • Graph Transformation
    • IR-54787
    • Abstract Interpretation
    • METIS-227742
    • EWI-1319
    • Software Model Checking

    Cite this

    Rensink, A., & Distefano, D. S. (2005). Abstract Graph Transformation. (CTIT Technical Report Series; No. 05-04). Enschede: Centre for Telematics and Information Technology (CTIT).
    Rensink, Arend ; Distefano, D.S. / Abstract Graph Transformation. Enschede : Centre for Telematics and Information Technology (CTIT), 2005. 25 p. (CTIT Technical Report Series; 05-04).
    @book{cad27da98f754f7595291eda75337390,
    title = "Abstract Graph Transformation",
    abstract = "Graphs may be used as representations of system states in operational semantics and model checking; in the latter context, they are being investigated as an alternative to bit vectors. The corresponding transitions are obtained as derivations from graph production rules. In this paper we propose an abstraction technique in this framework: the state graphs are contracted by collecting nodes that are sufficiently similar (resulting in smaller states and a finite state space) and the application of the graph production rules is lifted to this abstract level. Since graph abstractions and rule applications can all be computed completely automatically, we believe that this can be the core of a practically feasible technique for software model checking.",
    keywords = "Graph Transformation, IR-54787, Abstract Interpretation, METIS-227742, EWI-1319, Software Model Checking",
    author = "Arend Rensink and D.S. Distefano",
    note = "TR-CTIT-05-04",
    year = "2005",
    month = "1",
    language = "Undefined",
    series = "CTIT Technical Report Series",
    publisher = "Centre for Telematics and Information Technology (CTIT)",
    number = "05-04",
    address = "Netherlands",

    }

    Rensink, A & Distefano, DS 2005, Abstract Graph Transformation. CTIT Technical Report Series, no. 05-04, Centre for Telematics and Information Technology (CTIT), Enschede.

    Abstract Graph Transformation. / Rensink, Arend; Distefano, D.S.

    Enschede : Centre for Telematics and Information Technology (CTIT), 2005. 25 p. (CTIT Technical Report Series; No. 05-04).

    Research output: Book/ReportReportProfessional

    TY - BOOK

    T1 - Abstract Graph Transformation

    AU - Rensink, Arend

    AU - Distefano, D.S.

    N1 - TR-CTIT-05-04

    PY - 2005/1

    Y1 - 2005/1

    N2 - Graphs may be used as representations of system states in operational semantics and model checking; in the latter context, they are being investigated as an alternative to bit vectors. The corresponding transitions are obtained as derivations from graph production rules. In this paper we propose an abstraction technique in this framework: the state graphs are contracted by collecting nodes that are sufficiently similar (resulting in smaller states and a finite state space) and the application of the graph production rules is lifted to this abstract level. Since graph abstractions and rule applications can all be computed completely automatically, we believe that this can be the core of a practically feasible technique for software model checking.

    AB - Graphs may be used as representations of system states in operational semantics and model checking; in the latter context, they are being investigated as an alternative to bit vectors. The corresponding transitions are obtained as derivations from graph production rules. In this paper we propose an abstraction technique in this framework: the state graphs are contracted by collecting nodes that are sufficiently similar (resulting in smaller states and a finite state space) and the application of the graph production rules is lifted to this abstract level. Since graph abstractions and rule applications can all be computed completely automatically, we believe that this can be the core of a practically feasible technique for software model checking.

    KW - Graph Transformation

    KW - IR-54787

    KW - Abstract Interpretation

    KW - METIS-227742

    KW - EWI-1319

    KW - Software Model Checking

    M3 - Report

    T3 - CTIT Technical Report Series

    BT - Abstract Graph Transformation

    PB - Centre for Telematics and Information Technology (CTIT)

    CY - Enschede

    ER -

    Rensink A, Distefano DS. Abstract Graph Transformation. Enschede: Centre for Telematics and Information Technology (CTIT), 2005. 25 p. (CTIT Technical Report Series; 05-04).