%0 Conference Proceedings
%T A Hoare-Like Calculus Using the SROIQσ Logic on Transformations of Graphs
%+ Centre National de la Recherche Scientifique (CNRS)
%+ Université Grenoble Alpes [2016-2019] (UGA [2016-2019])
%+ Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE)
%A Brenas, Jon, Haël
%A Echahed, Rachid
%A Strecker, Martin
%Z Part 2: Track B: Logic, Semantics, Specification and Verification
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 8th IFIP International Conference on Theoretical Computer Science (TCS)
%C Rome, Italy
%Y Josep Diaz
%Y Ivan Lanese
%Y Davide Sangiorgi
%I Springer
%3 Theoretical Computer Science
%V LNCS-8705
%P 164-178
%8 2014-09-01
%D 2014
%R 10.1007/978-3-662-44602-7_14
%K Description Logic
%K Graph Transformation
%K Programming Language Semantics
%K Tableau Calculus
%Z Computer Science [cs]Conference papers
%X 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 ${\cal SROIQ}^\sigma$) is an extension of the Description Logic (DL) $\mathcal{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 ${\cal SROIQ}^\sigma$ formulas. The main challenge solved in this paper is to show that the resulting proof problems are decidable.
%G English
%Z TC 1
%Z TC 2
%Z WG 2.2
%2 https://inria.hal.science/hal-01402040/document
%2 https://inria.hal.science/hal-01402040/file/978-3-662-44602-7_14_Chapter.pdf
%L hal-01402040
%U https://inria.hal.science/hal-01402040
%~ UNIV-TLSE2
%~ UNIV-TLSE3
%~ CNRS
%~ SMS
%~ UT1-CAPITOLE
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-TC2
%~ IFIP-LNCS-8705
%~ IFIP-TCS
%~ IFIP-WG2-2
%~ IRIT
%~ IRIT-ACADIE
%~ IRIT-FSL
%~ TOULOUSE-INP
%~ UNIV-UT3
%~ UT3-INP
%~ UT3-TOULOUSEINP