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 = {International Symposium on Theoretical Aspects of Software Engineering (TASE)},
  editor    = {Jun Pang and Chenyi Zhang and Jifeng He and Jian Weng},
  pages     = {124--131},
  year =      2018,
  month =     {8},
  address =   {Guangzhou, China},
  doi       = {10.1109/TASE.2018.00024},
  url       = {http://martin-strecker.org/Publications/tase2018.html}

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