Conference Publication Details
Mandatory Fields
Cheng Z.;Monahan R.;Power J.
CEUR Workshop Proceedings
Verifying simplegt transformations using an intermediate verification language
Optional Fields
Automatic theorem proving Boogie Graph transformation Intermediate verification language Model transformation verification Simplegt
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.
Grant Details