| Year | 2015 |
|---|---|
| Type | Report |
| Status | Published |
| Authors | Andrei Arusoaie, Dorel Lucanu, David Nowak, Vlad Rusu |
Links
Abstract
Reachability Logic is a recently introduced formalism, which is currently used for defining the operational semantics of programming languages and for stating properties about program executions. In this paper we show how Reachability Logic can be adapted for stating properties of transition systems described by Rewriting-Logic specifications. We propose an automatic procedure for verifying Rewriting-Logic specifications against Reachability-Logic properties. We prove the soundness of the procedure and illustrate it by verifying a communication protocol specified in Maude.
BibTeX
@TechReport{name,
author = {Andrei Arusoaie and Dorel Lucanu and David Nowak and Vlad Rusu},
title = {Verifying Reachability-Logic Properties on Rewriting-Logic Specifications (Extended Version)},
institution = {Alexandru Ioan Cuza University, Faculty of Computer Science},
year = {2015},
number = {TR15-01},
month = {February},
note = {},
url = {http://thor.info.uaic.ro/~tr/tr.pl.cgi[TR15-01]}
}