A Constructor-Based Reachability Logic for Rewrite Theories

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.