Skip to Main content Skip to Navigation
Conference papers

Verifying Reachability-Logic Properties on Rewriting-Logic Specifications

Dorel Lucanu 1 Vlad Rusu 2 Andrei Arusoaie 2 David Nowak 3, 4 
2 DREAMPAL - Dynamic Reconfigurable Massively Parallel Architectures and Languages
Inria Lille - Nord Europe, CRIStAL - Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189
3 2XS - Extra Small Extra Safe
CRIStAL - Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189
Abstract : Rewriting Logic is a simply, flexible, and powerful framework for specifying and analysing concurrent systems. 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. Reachability Logic has its roots in a wider-spectrum framework, namely, in Rewriting Logic Semantics. In this paper we show how Reachability Logic can be adapted for stating properties of transition systems described by Rewriting-Logic specifications. We propose a 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download
Contributor : Pal Dream Connect in order to contact the contributor
Submitted on : Tuesday, June 2, 2015 - 11:08:50 AM
Last modification on : Wednesday, March 23, 2022 - 3:51:21 PM
Long-term archiving on: : Tuesday, April 25, 2017 - 12:03:19 AM


Files produced by the author(s)



Dorel Lucanu, Vlad Rusu, Andrei Arusoaie, David Nowak. Verifying Reachability-Logic Properties on Rewriting-Logic Specifications. Logic, Rewriting, and Concurrency - Festschrift Symposium in Honor of José Meseguer, Sep 2015, Urbana Champaign, United States. ⟨10.1007/978-3-319-23165-5_21⟩. ⟨hal-01158941⟩



Record views


Files downloads