DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2016.14

Proving Correctness of Logically Decorated Graph Rewriting Systems

Authors: Jon Haël Brenas, Rachid Echahed, and Martin Strecker

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Abstract

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.

Cite as

Jon Haël Brenas, Rachid Echahed, and Martin Strecker. Proving Correctness of Logically Decorated Graph Rewriting Systems. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 14:1-14:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{brenas_et_al:LIPIcs.FSCD.2016.14,
  author =	{Brenas, Jon Ha\"{e}l and Echahed, Rachid and Strecker, Martin},
  title =	{{Proving Correctness of Logically Decorated Graph Rewriting Systems}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{14:1--14:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.14},
  URN =		{urn:nbn:de:0030-drops-59778},
  doi =		{10.4230/LIPIcs.FSCD.2016.14},
  annote =	{Keywords: Graph Rewriting, Hoare Logic,Combinatory PDL, Rewrite Strategies, Program Verification}
}

Search Results

Documents authored by Brenas, Jon Haël

Proving Correctness of Logically Decorated Graph Rewriting Systems

Abstract

Cite as

Thanks for your feedback!

Could not send message