Files in this item



application/pdfcoh-compl-journal.pdf (716kB)
(no description provided)PDF


Title:Generalized Rewrite Theories, Coherence Completion and Symbolic Methods
Author(s):Meseguer, Jose
Subject(s):generalized rewrite theories
pattern predicates
constrained narrowing
symbolic invariant verification
Abstract:A new notion of generalized rewrite theory suitable for symbolic reasoning and generalizing the standard notion is motivated and defined. Also, new requirements for symbolic executability of generalized rewrite theories that extend those for standard rewrite theories, including a generalized notion of coherence, are given. Symbolic executability, including coherence, is both ensured and made available for a wide class of such theories by automatable theory transformations. Using these foundations, several symbolic reasoning methods using generalized rewrite theories are studied, including: (i) symbolic description of sets of terms by pattern predicates; (ii) reasoning about universal reachability properties by generalized rewriting; (iii) reasoning about existential reachability properties by constrained narrowing; and (iv) symbolic verification of safety properties such as invariants and stability properties.
Issue Date:2018-12-19
Genre:Technical Report
Sponsor:This work has been partially supported by NRL under contract number N00173-17-1-G002.
Date Available in IDEALS:2018-12-19

This item appears in the following Collection(s)

Item Statistics