r10

V. Rusu. Combining narrowing and theorem proving for rewriting-logic specifications. In 4th International Conference on Tests and Proofs (Tap'10), LNCS, Volume 6143, Pages 135-150, July 2010.

Download [help]

Download paper: Doi page

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 for verifying dynamic systems specified in rewriting logic, a formal specification language implemented in the Maude system. Our approach is tailored for invariants, i.e., properties that hold on all states reachable from a given class of initial states. The approach consists in encoding invariance properties into inductive properties written in membership equational logic, a sublogic of rewriting logic also implemented in Maude. The invariants can then be verified using an inductive theorem prover available for membership equational logic, possibly in interaction with narrowing-based symbolic analysis tools for rewriting-logic specifications also available in the Maude environment. We show that it is possible, and useful, to automatically test invariants by symbolic analysis before interactively proving them

Contact

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

BibTex Reference

@InProceedings{r10,
   Author = {Rusu, V.},
   Title = {Combining narrowing and theorem proving for rewriting-logic specifications},
   BookTitle = {4th International Conference on Tests and Proofs (Tap'10)},
   Volume = {6143},
   Pages = {135--150},
   Series = {LNCS},
   Publisher = {Springer},
   Month = {July},
   Year = {2010}
}

EndNote Reference [help]

Get EndNote Reference (.ref)