%0 Conference Proceedings
%F r10
%A Rusu, V.
%T Combining narrowing and theorem proving for rewriting-logic specifications
%B 4th International Conference on Tests and Proofs (Tap'10)
%V 6143
%P 135-150
%S LNCS
%I Springer
%X 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
%U http://www.irisa.fr/vertecs/Publis/Ps/2010-tap.pdf
%U http://dx.doi.org/10.1007/978-3-642-13977-2_12
%8 July
%D 2010