up: Publications |
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.
Online Copy |
BibTeX Entry |
@inproceedings{brenas16:_provin_correc_logic_decor_graph_rewrit_system, author = {Jon Ha{\"{e}}l Brenas and Rachid Echahed and Martin Strecker}, title = {Proving Correctness of Logically Decorated Graph Rewriting Systems}, booktitle = {1st International Conference on Formal Structures for Computation and Deduction, {FSCD} 2016, June 22-26, 2016, Porto, Portugal}, editor = {Delia Kesner and Brigitte Pientka}, series = {LIPIcs}, volume = {52}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik}, pages = {14:1--14:15}, year = 2016, url = {http://dx.doi.org/10.4230/LIPIcs.FSCD.2016.14}, doi = {10.4230/LIPIcs.FSCD.2016.14} }
Tue Oct 25 11:40:23 CEST 2016 |