1 Search Results for "Brenas, Jon Haël"


Document
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-dev.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}
}
  • Refine by Author
  • 1 Brenas, Jon Haël
  • 1 Echahed, Rachid
  • 1 Strecker, Martin

  • Refine by Classification

  • Refine by Keyword
  • 1 Graph Rewriting
  • 1 Hoare Logic,Combinatory PDL
  • 1 Program Verification
  • 1 Rewrite Strategies

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2016

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail