Vérification et réécriture

Michaël Rusinowitch 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : Nous présenterons quelques applications de la réécriture en vérification. Typiquement un certain nombre de procédures de décision utilisées par les assistants de preuve peuvent être obtenues de manière uniforme en généralisant la complétion de Knuth-Bendix. La réécriture permet également la construction de tactiques d'induction intéressantes pour la preuves d'invariants. Ces tactiques détectent plus facilement les conjectures fausses. Enfin nous présenterons une application de la réécriture à la vérification de protocoles de sécurité. Ces protocoles se compilent en règles de réécriture qui expriment de manière très naturelle le comportement des principaux ou de l'intrus.
Type de document :
Communication dans un congrès
Journées Systèmes Infinis, 2001, Paris, France, 2001
Liste complète des métadonnées

https://hal.inria.fr/inria-00100557
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:47:32
Dernière modification le : jeudi 11 janvier 2018 - 06:19:57

Identifiants

  • HAL Id : inria-00100557, version 1

Collections

Citation

Michaël Rusinowitch. Vérification et réécriture. Journées Systèmes Infinis, 2001, Paris, France, 2001. 〈inria-00100557〉

Partager

Métriques

Consultations de la notice

97