Jump to : Abstract | Contact | BibTex reference | EndNote reference |
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.
Vlad Rusu
Vlad.Rusu@irisa.fr
@TechReport{rc07,
Author = {Rusu, V. and Clavel, M.},
Title = {Theorem proving for Maude's Rewriting Logic},
Number = {1873},
Institution = {Irisa},
Year = {2007}
}
Get EndNote Reference (.ref)