Skip to Main content Skip to Navigation
Conference papers

Combining theorem proving and narrowing for rewriting-logic specifications

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download
Contributor : Mister Dart Connect in order to contact the contributor
Submitted on : Wednesday, October 20, 2010 - 3:08:00 PM
Last modification on : Friday, February 4, 2022 - 3:08:47 AM
Long-term archiving on: : Friday, October 26, 2012 - 11:46:30 AM


Files produced by the author(s)


  • HAL Id : inria-00527864, version 1



Vlad Rusu. Combining theorem proving and narrowing for rewriting-logic specifications. International Conference on Tests and Proofs, 2010, Malaga, Spain. ⟨inria-00527864⟩



Record views


Files downloads