A Constructor-Based Reachability Logic for Rewrite Theories
Abstract
Reachability logic has been applied to 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.
Cite
@article{arxiv.1709.05045,
title = {A Constructor-Based Reachability Logic for Rewrite Theories},
author = {Stephen Skeirik and Andrei Stefanescu and José Meseguer},
journal= {arXiv preprint arXiv:1709.05045},
year = {2017}
}
Comments
Pre-proceedings paper presented at the 27th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2017), Namur, Belgium, 10-12 October 2017 (arXiv:1708.07854)