Provably Correct Graph Transformations with Small-tALC

We present a prototype for executing and verifying graph transformations. The transformations are written in a simple imperative programming language, and pre- and post-conditions as well as loop invariants are specified in the Description Logic ALC (whence the name of the tool). The programming language has a precisely defined operational semantics and a sound Hoare-style calculus. The tool consists of the following sub-components: a compiler to Java for executing the transformations; a verification condition generator; and a tableau prover for an extension of ALC capable of deciding the generated verification conditions. A description of these components and their interaction is the main purpose of this paper.
 

Online Copy

Online version

Formal development

BibTeX Entry

@inproceedings{baklanova15:_provab_correc_graph_trans_small,
  author    = {Nadezhda Baklanova and
               Jon Ha{\"{e}}l Brenas and
               Rachid Echahed and
               Christian Percebois and
               Martin Strecker and
               Hanh Nhi Tran},
  title     = {Provably Correct Graph Transformations with Small-tALC},
  booktitle = {Proceedings of the 11th International Conference on {ICT} in Education,
               Research and Industrial Applications: Integration, Harmonization and
               Knowledge Transfer, Lviv, Ukraine, May 14-16, 2015.},
  pages     = {78--93},
  year      = 2015,
  url       = {http://www.irit.fr/~Martin.Strecker/Publications/icteri2015.html}
}