Neighbourhood Abstraction in GROOVE - Tool Paper

Arend Rensink, Eduardo Zambon

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    17 Downloads (Pure)

    Abstract

    In this paper we discuss the implementation of neighbourhood graph abstraction in the GROOVE tool set. Important classes of graph grammars may have unbounded 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 presented the theory of neighbourhood abstraction. In this paper, we present the implementation of this theory in GROOVE and illustrate its applicability with a case study that models a single-linked list.
    Original languageUndefined
    Title of host publicationProceedings of the Fourth International Workshop on Graph-Based Tools (GraBaTs 2010)
    EditorsJuan de Lara, Daniel Varro
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Pages55-61
    Number of pages6
    Publication statusPublished - Jun 2010
    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

    Publication series

    NameCTIT Workshop Proceedings
    PublisherCentre for Telematics and Information Technology University of Twente
    NumberWP 10-06
    ISSN (Print)0929-0672
    ISSN (Electronic)0929-0672

    Conference

    ConferenceFourth International Workshop on Graph-Based Tools, GraBaTs 2010
    Abbreviated titleGraBaTs 2010
    CountryNetherlands
    CityEnschede
    Period28/09/1028/09/10
    Other28 September 2010

    Keywords

    • METIS-276081
    • GROOVE
    • Model Checking
    • EWI-18316
    • Graph Abstraction
    • Graph Transformation
    • IR-72606

    Cite this