Neighbourhood Abstraction in GROOVE

Arend Rensink, Eduardo Zambon

    Research output: Contribution to journalConference articleAcademicpeer-review

    9 Citations (Scopus)

    Abstract

    Important classes of graph grammars have infinite state spaces and therefore cannot be verified with traditional model checking techniques. One way to address this problem is to perform graph abstraction, which allows us to generate a finite abstract state space that over-approximates the original one. In previous work we developed the theory of neighbourhood abstraction. In this paper, we present the implementation of this theory in GROOVE and illustrate its use with a small grammar that models operations on a single-linked list.
    Original languageEnglish
    Pages (from-to)1-13
    Number of pages13
    JournalEASST electronic communications
    Volume32
    DOIs
    Publication statusPublished - 11 Apr 2011
    EventFourth International Workshop on Graph-Based Tools, GraBaTs 2010: Proceedings of the Fourth International Workshop on Graph-Based Tools (GraBaTs 2010) - University of Twente, Enschede, Netherlands
    Duration: 28 Sep 201028 Sep 2010
    Conference number: 4

    Keywords

    • IR-76652
    • METIS-270989
    • Graph Abstraction
    • EWI-20018
    • GROOVE
    • Model Checking
    • Graph Transformation

    Fingerprint Dive into the research topics of 'Neighbourhood Abstraction in GROOVE'. Together they form a unique fingerprint.

    Cite this