Files in this item



application/pdfreach-log.pdf (487kB)
(no description provided)PDF


Title:A Constructor-Based Reachability Logic for Rewrite Theories
Author(s):Skeirik, Stephen; Stefanescu, Andrei; Meseguer, José
Subject(s):reachability and rewriting logics, program verification
Abstract:Reachability logic has been applied to K rewrite-rule-based language definitions as a language-generic logic of programs. It has been proved successful in verifying a wide range of sophisticated programs in conventional languages. Here we study how reachability logic can be made not just language-generic, but rewrite-theory-generic to make it available not just for conventional program verification, but also to verify rewriting-logic-based programs and distributed system designs. 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, 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.
Issue Date:2017-03-27
Genre:Technical Report
Sponsor:Partially supported by NSF Grants CNS 13-19109 and CNS 14-09416, and AFOSR Contract FA8750-11-2-0084.
Rights Information:Copyright held by Stephen Skeirik, Andrei Stefanescu and Jose Meseguer
Date Available in IDEALS:2017-03-27

This item appears in the following Collection(s)

Item Statistics