## Files in this item

FilesDescriptionFormat

application/pdf

tr.pdf (685kB)
Updated file Feb 23 2011PDF

## Description

 Title: Proving Safety Properties of Rewrite Theories Author(s): Rocha, Camilo; Meseguer, José Subject(s): Safety properties Ground invariance Ground stability Rewrite theories Inductive theorem proving Maude Invariant Analyzer Tool - InvA Abstract: Rewriting logic theories are a general and expressive way of specifying concurrent systems, where states are axiomatized by equations and transitions among states are axiomatized by rewrite rules. In this paper, we present a {\em transformational} and {\em reductionistic} deductive approach for verifying {\em safety properties} of rewrite theories. In our approach all formal temporal reasoning about concurrent transitions is ultimately reduced to purely equational inductive reasoning. Narrowing modulo axioms is extensively used to simplify the equational proof obligations to which all proofs of safety formulas are ultimately reached. This allows these generic verification methods to take advantage of the existing wealth of equational reasoning techniques and tools already available. We report on the implementation of this deductive system in the Maude Invariant Analyzer tool, which provides a substantial degree of automation and can automatically discharge many proof obligations without user intervention. Issue Date: 2010-11-18 Genre: Technical Report Type: Text Language: English URI: http://hdl.handle.net/2142/17407 Publication Status: unpublished Peer Reviewed: not peer reviewed Date Available in IDEALS: 2010-11-18
﻿