Ensemble de termes accessibles en réécriture : aux frontières de la régularité - DUMAS - Dépôt Universitaire de Mémoires Après Soutenance
Master Thesis Year : 2011

Ensemble de termes accessibles en réécriture : aux frontières de la régularité

Abstract

Avant d'exploiter ou de diffuser un logiciel, il convient de s'assurer de sa correction. Lorsque la taille du programme est grande, l'automatisation de la preuve est à rechercher, mais elle ne peut être une panacée (théorème de Rice). Ce rapport s'inscrit dans une étude utilisant les systèmes de réécriture (TRS) comme modèles formels des programmes : la correction s'exprime par le fait que l'ensemble des termes accessibles par le TRS considéré est disjoint d'un ensemble de termes représentant les mauvais comportements. On sait décider une telle propriété si les langages en jeu sont réguliers (au sens des automates d'arbres). Certaines classes de TRS préservant la régularité sont connues mais ne couvrent pas tous les cas. Ici, nous nous intéressons à la complétion d'automate. La complétion équationnelle permet de paramétrer la sur-approximation par un ensemble $E$ d'équations entre termes afin de favoriser l'obtention d'un point fixe. Nous exposons cette méthode et tentons de l'exprimer dans le vocabulaire de l'interprétation abstraite, une autre méthode d'élaboration d'analyses statiques.
Fichier principal
Vignette du fichier
Salmon.pdf (377.11 Ko) Télécharger le fichier
Loading...

Dates and versions

dumas-00636806 , version 1 (28-10-2011)

Identifiers

  • HAL Id : dumas-00636806 , version 1

Cite

Yann Salmon. Ensemble de termes accessibles en réécriture : aux frontières de la régularité. Théorie et langage formel [cs.FL]. 2011. ⟨dumas-00636806⟩
102 View
175 Download

Share

More