up: Publications

Verifying Graph Transformations with Guarded Logics

Jon Haël Brenas, Rachid Echahed, Martin Strecker


We consider the problem of verifying graph transformations described by an imperative programming language. This question is particularly relevant for transformation of knowledge bases. We will argue in this paper that previous proof approaches based on dedicated Description Logics were technically complex and often inappropriate for reasoning about preservation of structure of knowledge bases. For these reasons, we explore here an assertion formalism based on the Guarded Fragment of predicate logic, which provides a homogeneous framework. Based on a formal semantics of our transformation language, we show how to extract proof obligations from annotated programs and how to obtain decidable correctness problems.
 Online Copy

BibTeX Entry

  author =       {Jon Haël Brenas and
               Rachid Echahed and
               Martin Strecker},
  title =        {Verifying Graph Transformations with Guarded Logics},
  booktitle = {Proceedings of the 12th International Symposium on Theoretical Aspects of Software Engineering},
  year =      2018,
  month =     {8},
  address =   {Guangzhou, China}

Last modified: Wed Oct 17 01:07:36 CEST 2018