Verifying Graph Transformations with Guarded Logics

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

• Conference paper: (personal copy) (publisher's version)

BibTeX Entry

@InProceedings{brenas18:_verif_graph_trans_guard_logic,
  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}
}