OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Proving Correctness of Logically Decorated Graph Rewriting Systems

Brenas, Jon Haël and Echahed, Rachid and Strecker, Martin Proving Correctness of Logically Decorated Graph Rewriting Systems. (2016) In: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), 22 June 2016 - 26 June 2016 (Porto, Portugal).

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: https://doi.org/10.4230/LIPIcs.FSCD.2016.14


We first introduce the notion of logically decorated rewriting systems where the left-hand sides are endowed with logical formulas which help to express positive as well as negative application conditions, in addition to classical pattern-matching. These systems are defined using graph structures and an extension of combinatory propositional dynamic logic, CPDL, with restricted universal programs, called C2PDL. In a second step, we tackle the problem of proving the correctness of logically decorated graph rewriting systems by using a Hoare-like calculus. We introduce a notion of specification defined as a tuple (Pre, Post, R, S) with Pre and Post being formulas of C2PDL, R a rewriting system and S a rewriting strategy. We provide a sound calculus which infers proof obligations of the considered specifications and establish the decidability of the verification problem of the (partial) correctness of the considered specifications.

Item Type:Conference or Workshop Item (Paper)
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
Other partners > Université Grenoble Alpes - UGA (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:
Deposited On:08 Mar 2019 14:27

Repository Staff Only: item control page