A Constructor-Based Reachability Logic for Rewrite Theories

TL;DR

This paper introduces a new constructor-based reachability logic for rewrite theories, enhancing verification capabilities for distributed systems and improving automation through semantic unification and matching techniques.

Contribution

It presents a rewrite-theory-generic reachability logic, proves its soundness, and develops new methods for invariant proofs in distributed systems, supported by a prototype implementation.

Findings

Soundness of the new logic for a wide class of rewrite theories

Enhanced automation via constructor-based semantic procedures

Successful experiments demonstrating the proof methods

Abstract

Reachability logic has been applied to $\mathbb{K}$ rewrite-rule-based language definitions as a language-generic logic of programs. To be able to verify not just code but also distributed system designs, a new rewrite-theory-generic reachability logic is presented and proved sound for a wide class of rewrite theories. The logic's automation is increased by means of constructor-based semantic unification, matching, and satisfiability procedures. New methods for proving invariants of possibly never terminating distributed systems are developed, and experiments with a prototype implementation illustrating the new proof methods are presented.