Files in this item



application/pdftr.pdf (685kB)
Updated file Feb 23 2011PDF


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
Publication Status:unpublished
Peer Reviewed:not peer reviewed
Date Available in IDEALS:2010-11-18

This item appears in the following Collection(s)

Item Statistics