TY - JOUR
T1 - A Constructor-Based Reachability Logic for Rewrite Theories
AU - Skeirik, Stephen
AU - Stefanescu, Andrei
AU - Meseguer, José
N1 - Funding Information:
We have implemented the reachability logic proof system in Maude [34]. We exploit the fact that rewriting logic is reflective, so that concepts such as terms, rewrite rules, signatures, and theories are directly expressible as data in the logic. This is supported by Maude’s META-LEVEL library [34]. Our prototype tool takes as input (i) a reflected rewrite theory R pΣ, E Y B, Rq and (ii) a set of reachability formulas C tAi Ñf BiuiPI to be simultaneously proved.
Funding Information:
We thank Grigore Ro?u, Dorel Lucanu and Vlad Rusu for their very helpful comments on an earlier draft of this work, and the anonymous referees for numerous judicious comments that have also helped to substantially improve the paper. This research has been partially supported by NSF Grants CNS 13-19109 and CNS 14-09416, AFOSR Contract FA8750-11-2-0084, and NRL under contract N00173-17-1-G002.
Publisher Copyright:
© 2020 - IOS Press and the authors. All rights reserved.
PY - 2020
Y1 - 2020
N2 - 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.
AB - 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.
KW - deductive verification
KW - reachability and rewriting logics
UR - http://www.scopus.com/inward/record.url?scp=85082992989&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85082992989&partnerID=8YFLogxK
U2 - 10.3233/FI-2020-1926
DO - 10.3233/FI-2020-1926
M3 - Article
AN - SCOPUS:85082992989
SN - 0169-2968
VL - 173
SP - 315
EP - 382
JO - Fundamenta Informaticae
JF - Fundamenta Informaticae
IS - 4
ER -