A Constructor-Based Reachability Logic for Rewrite Theories

Stephen Skeirik, Andrei Stefanescu, José Meseguer

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 dis…