A Constructor-Based Reachability Logic for Rewrite Theories

Skeirik, Stephen; Stefanescu, Andrei; Meseguer, José

Permalink

https://hdl.handle.net/2142/95770 Copy

Description

Title

A Constructor-Based Reachability Logic for Rewrite Theories

Author(s)

• Skeirik, Stephen
• Stefanescu, Andrei
• Meseguer, José

Issue Date

2017-03-27

Keyword(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.

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/95770

Sponsor(s)/Grant Number(s)

Partially supported by NSF Grants CNS 13-19109 and CNS 14-09416, and AFOSR Contract FA8750-11-2-0084.

Copyright and License Information

Copyright held by Stephen Skeirik, Andrei Stefanescu and Jose Meseguer

Owning Collections