Decidable Approximations of Sets of Descendants and Sets of Normal forms

Thomas Genet 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : A partir de techniques d'automates d'arbres, nous présentons des approximations calculables des ensembles de descendants et des ensembles de formes normales d'un système de réécriture. Dans le contexte de la logique de réécriture, un système de réécriture est un programme et une forme normale est un résultat du programme. Ainsi, l'approximation de l'ensemble des descendants et de l'ensemble des formes normales, fournit des outils pour la vérification des programmes : nous montrons en particulier comment calculer un sur-ensemble des résultats, comment montrer la complétude suffisante, ou encore comment prouver la terminaison sous une stratégie précise, la stratégie de réduction séquentielle.
Type de document :
Communication dans un congrès
9th Conference on Rewriting Techniques and Applications, 1998, Tsukuba, Japan, Springer-Verlag, 1379, pp.151-165, 1998, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00098700
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:17:53
Dernière modification le : mardi 24 avril 2018 - 14:12:05
Document(s) archivé(s) le : mercredi 29 mars 2017 - 12:29:25

Fichiers

Identifiants

  • HAL Id : inria-00098700, version 1

Citation

Thomas Genet. Decidable Approximations of Sets of Descendants and Sets of Normal forms. 9th Conference on Rewriting Techniques and Applications, 1998, Tsukuba, Japan, Springer-Verlag, 1379, pp.151-165, 1998, Lecture Notes in Computer Science. 〈inria-00098700〉

Partager

Métriques

Consultations de la notice

109

Téléchargements de fichiers

76