up: Publications

A Hoare-like calculus using the SROIQσ logic on transformations of graphs

Jon-Hael Brenas, Rachid Echahed, Martin Strecker

TCS 2014


We tackle the problem of partial correctness of programs processing structures defined as graphs. We introduce a kernel imperative programming language endowed with atomic actions that participate in the transformation of graph structures and provide a decidable logic for reasoning about these transformations in a Hoare-style calculus. The logic for reasoning about the transformations (baptized SROIQσ) is an extension of the Description Logic (DL) SROIQ, and the graph structures manipulated by the programs are models of this logic. The programming language is non-standard in that it has an instruction set targeted at graph manipulations (such as insertion and deletion of arcs), and its conditional statements (in loops and selections) are SROIQσ formulas. The main challenge solved in this paper is to show that the resulting proof problems are decidable.
Online Copy

Additional material
BibTeX Entry
  author =       {Brenas, Jon Haël and Echahed, Rachid and Strecker, Martin},
  title =        {A Hoare-Like Calculus Using the ${\cal SROIQ}^\sigma$ Logic on
                  Transformations of Graphs},
  year =         2014,
  isbn =         {978-3-662-44601-0},
  booktitle =    {Theoretical Computer Science},
  volume =       8705,
  series =       {Lecture Notes in Computer Science},
  editor =       {Diaz, Josep and Lanese, Ivan and Sangiorgi, Davide},
  doi =          {10.1007/978-3-662-44602-7_14},
  url =          {http://www.irit.fr/~Martin.Strecker/Publications/tcs2014.html},
  publisher =    {Springer Berlin Heidelberg},
  keywords =     {Description Logic; Graph Transformation; Programming
                  Language Semantics; Tableau Calculus},
  pages =        {164-178}

Last modified: Mon Sep 1 10:07:21 CEST 2014