Vérification et réécriture - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2001

Vérification et réécriture

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.

Domaines

Autre [cs.OH]
Fichier non déposé

Dates et versions

inria-00100557 , version 1 (26-09-2006)

Identifiants

  • HAL Id : inria-00100557 , version 1

Citer

Michaël Rusinowitch. Vérification et réécriture. Journées Systèmes Infinis, A. Bouajjani, 2001, Paris, France. ⟨inria-00100557⟩
86 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More