Generalized Rewrite Theories, Coherence Completion and Symbolic Methods

Meseguer, José

Permalink

https://hdl.handle.net/2142/102183 Copy

Description

Title

Generalized Rewrite Theories, Coherence Completion and Symbolic Methods

Author(s)

Meseguer, José

Issue Date

2018-12-19

Keyword(s)

• generalized rewrite theories
• coherence
• variants
• 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.

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/102183

Sponsor(s)/Grant Number(s)

This work has been partially supported by NRL under contract number N00173-17-1-G002.

Owning Collections