Verification Techniques for Graph Rewriting (Tutorial)

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

    29 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

    Publication series

    NameDagstuhl Reports
    PublisherDagstuhl Publishing
    ISSN (Print)2192-5283


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

    Cite this

    Rensink, A. (2016). Verification Techniques for Graph Rewriting (Tutorial). In P. A. Abdulla, F. Gadducci, B. König, & V. Vafeiadis (Eds.), Verification of Evolving Graph Structures (pp. 18-18). (Dagstuhl Reports; Vol. 5, No. 11). Dagstuhl, Germany: Dagstuhl.