Proving Safety Properties of Rewrite Theories

Rocha, Camilo; Meseguer, José

Permalink

https://hdl.handle.net/2142/17407 Copy

Description

Title

Proving Safety Properties of Rewrite Theories

Author(s)

• Rocha, Camilo
• Meseguer, José

Issue Date

2010-11-18

Keyword(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.

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/17407

Owning Collections