TR15-01 (2015) – Verifying Reachability-Logic Properties on Rewriting-Logic Specifications (Extended Version)

Andrei Arusoaie, Dorel Lucanu, David Nowak, Vlad Rusu

Reachability Logic is a recently introduced formalism, whichis currently used for defining the operational semantics of programminglanguages and for stating properties about program executions. In thispaper we show how Reachability Logic can be adapted for stating propertiesof transition systems described by Rewriting-Logic specifications.We propose an automatic procedure for verifying Rewriting-Logic specificationsagainst Reachability-Logic properties. We prove the soundnessof the procedure and illustrate it by verifying a communication protocolspecified in Maude.

Bibtex

@TechReport{vrlprls,
author = "Andrei Arusoaie and Dorel Lucanu and David Nowak and Vlad Rusu",
title = "{Verifying Reachability-Logic Properties on Rewriting-Logic Specifications (Extended Version)}",
institution = "``Al.I.Cuza'' University of Ia{c s}i,
                 Faculty of Computer Science",
year = "2015",
number = "TR 15-01",
note = "url{http://www.infoiasi.ro/~tr/tr.pl.cgi}"
}