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

https://hal.inria.fr/inria-00527864
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

File

2010-tap.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00527864, version 1

Collections

Citation

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

Share

Metrics

Record views

58

Files downloads

123