A Constructor-Based Reachability Logic for Rewrite Theories

Stephen Skeirik, Andrei Stefanescu, José Meseguer

Research output: Contribution to journalArticle

Abstract

Reachability logic has been applied to rewrite-rule-based language definitions as a language-generic logic of programs to verify a wide range of sophisticated programs in conventional languages. Here we study how reachability logic can be made not just language-generic, but also rewrite-theory-generic, so that we can verify both conventional programs based on their rewriting logic operational semantics and distributed system designs specified as rewrite theories. A theory-generic reachability logic is presented and proved sound for a wide class of rewrite theories. Particular attention is given to increasing the logic's automation by means of constructor-based semantic unification, matching, narrowing, and satisfiability procedures. The relationships to Hoare logic and LTL are discussed, new methods for proving invariants of possibly never terminating distributed systems are developed, and experiments with a prototype implementation illustrating the new methods are presented.

Original languageEnglish (US)
Pages (from-to)315-382
Number of pages68
JournalFundamenta Informaticae
Volume173
Issue number4
DOIs
StatePublished - Jan 1 2020

    Fingerprint

Keywords

  • deductive verification
  • reachability and rewriting logics

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Algebra and Number Theory
  • Information Systems
  • Computational Theory and Mathematics

Cite this