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.
Type de document :
Communication dans un congrès
International Conference on Tests and Proofs, 2010, Malaga, Spain. Springer Verlag, 2010
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00527864
Contributeur : Mister Dart <>
Soumis le : mercredi 20 octobre 2010 - 15:08:00
Dernière modification le : mercredi 11 avril 2018 - 01:54:05
Document(s) archivé(s) le : vendredi 26 octobre 2012 - 11:46:30

Fichier

2010-tap.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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. Springer Verlag, 2010. 〈inria-00527864〉

Partager

Métriques

Consultations de la notice

168

Téléchargements de fichiers

138