Generalized rewrite theories, coherence completion, and symbolic methods

Research output: Contribution to journalArticle

Abstract

A new notion of generalized rewrite theory suitable for symbolic reasoning and generalizing the standard notion in [19] is motivated and defined. Also, new requirements for symbolic executability of generalized rewrite theories that extend those in [33] 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.

Original languageEnglish (US)
Article number100483
JournalJournal of Logical and Algebraic Methods in Programming
Volume110
DOIs
StatePublished - Jan 2020

Keywords

  • Coherence
  • Constrained narrowing
  • Generalized rewrite theories
  • Pattern predicates
  • Symbolic invariant verification

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Software
  • Logic
  • Computational Theory and Mathematics

Fingerprint Dive into the research topics of 'Generalized rewrite theories, coherence completion, and symbolic methods'. Together they form a unique fingerprint.

  • Cite this