Verification Techniques for Graph Rewriting (Tutorial)

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic

    106 Downloads (Pure)


    This tutorial paints a high-level picture of the concepts involved in verification of graph transformation systems. We distinguish three fundamentally different application scenarios for graph rewriting: (1) as grammars (in which case we are interested in the language, or set, of terminal graphs for a fixed start graph); (2) as production systems (in which case we are interested in the relation between start and terminal graphs); or (3) as behavioural specifications (in which case we are interested in the transition system as a whole). We then list some types of questions one might want to answer through verification: confluence and termination, reachability, temporal properties, or contractual properties. Finally, we list some techniques that can help in providing answers: model checking, unfolding, assertional reasoning, and abstraction.
    Original languageUndefined
    Title of host publicationVerification of Evolving Graph Structures
    EditorsParosh Aziz Abdulla, Fabio Gadducci, Barbara König, Viktor Vafeiadis
    Place of PublicationDagstuhl, Germany
    Number of pages1
    Publication statusPublished - Mar 2016
    EventVerification of Evolving Graph Structures - Dagstuhl, Germany
    Duration: 1 Nov 20156 Nov 2015

    Publication series

    NameDagstuhl Reports
    PublisherDagstuhl Publishing
    ISSN (Print)2192-5283


    WorkshopVerification of Evolving Graph Structures
    Other1-6 November 2015


    • EWI-26905
    • METIS-316865
    • IR-100130

    Cite this