rc07

V. Rusu, M. Clavel. Theorem proving for Maude's Rewriting Logic. Research Report Irisa, No 1873, 2007.

Download [help]

Download paper: Adobe portable document (pdf)

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic

Abstract

We present an approach based on inductive theorem proving for verifying invariance properties of systems specified in Rewriting Logic, an executable specification language implemented (among others) in the Maude tool. Since theorem proving is not directly available for rewriting logic, we define an encoding of rewriting logic into its membership equational (sub)logic. Then, inductive theorem provers for membership equational logic, such as the ITP tool, can be used for verifying the resulting membership equational logic specification, and, implicitly, for verifying invariance properties of the original rewriting logic specification. The approach is illustrated first on a 2-process Bakery algorithm and then on a parameterised, n-process version of the algorithm

Contact

Vlad Rusu http://www.irisa.fr/vertecs/Equipe/Rusu/vlad-rusu.html

BibTex Reference

@TechReport{rc07,
   Author = {Rusu, V. and Clavel, M.},
   Title = {Theorem proving for Maude's Rewriting Logic},
   Number = {1873},
   Institution = {Irisa},
   Year = {2007}
}

EndNote Reference [help]

Get EndNote Reference (.ref)