MURAL - Maynooth University Research Archive Library

    Verifying SimpleGT Transformations Using an Intermediate Verification Language

    Cheng, Zheng and Monahan, Rosemary and Power, James F. (2016) Verifying SimpleGT Transformations Using an Intermediate Verification Language. In: 4th International Workshop on the Verification Of Model Transformations, Jully 2015, L'Aquila, Italy.

    Download (251kB) | Preview

    Share your research

    Twitter Facebook LinkedIn GooglePlus Email more...

    Add this article to your Mendeley library


    Previously, we have developed the VerMTLr framework that allows rapid verifier construction for relational model transformation languages. VerMTLr draws on the Boogie intermediate verification language to systematically design a modular and reusable verifier. It also includes a modular formalisation of EMFTVM bytecode to ensure verifier soundness. In this work, we will illustrate how to adapt VerMTLr to design a verifier for the SimpleGT graph transformation language, which allows us to soundly prove the correctness of graph transformations. An experiment with the Pacman game demonstrates the feasibility of our approach.

    Item Type: Conference or Workshop Item (Paper)
    Keywords: model transformation verification; graph transformation; SimpleGT; automatic theorem proving; intermediate verification language; Boogie;
    Academic Unit: Faculty of Science and Engineering > Computer Science
    Item ID: 8220
    Depositing User: Dr. James Power
    Date Deposited: 17 May 2017 15:37
    Refereed: Yes
      Use Licence: This item is available under a Creative Commons Attribution Non Commercial Share Alike Licence (CC BY-NC-SA). Details of this licence are available here

      Repository Staff Only(login required)

      View Item Item control page


      Downloads per month over past year

      Origin of downloads