Title :

Verifying Reachability-Logic Properties on Rewriting-Logic Specifications

Author(s) :

Lucanu, Dorel [Auteur]
Department of Computer Science [Lasi]
Rusu, Vlad [Auteur]
Dynamic Reconfigurable Massively Parallel Architectures and Languages [DREAMPAL]
Arusoaie, Andrei [Auteur]
Dynamic Reconfigurable Massively Parallel Architectures and Languages [DREAMPAL]
Nowak, David [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Extra Small Extra Safe [2XS]

Conference title :

Logic, Rewriting, and Concurrency - Festschrift Symposium in Honor of José Meseguer

City :

Urbana Champaign

Country :

Etats-Unis d'Amérique

Start date of the conference :

2015-09-23

Book title :

LNCS

Journal title :

Logic, Rewriting, and Concurrency Essays Dedicated to José Meseguer on the Occasion of His 65th Birthday

Publisher :

Springer Verlag

Publication date :

2015

HAL domain(s) :

Informatique [cs]/Logique en informatique [cs.LO]

English abstract : [en]

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 ...
Show more >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.Show less >

Language :

Anglais

Peer reviewed article :

Oui

Audience :

Internationale

Popular science :

Non

Collections :

• Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL