Skip to Main content Skip to Navigation
Master Thesis

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

Résumé : 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.
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download

https://dumas.ccsd.cnrs.fr/dumas-00636806
Contributor : Co-Responsables Du Mri V. Gouranton Et S. Blazy <>
Submitted on : Friday, October 28, 2011 - 12:19:20 PM
Last modification on : Monday, February 15, 2021 - 10:37:44 AM
Long-term archiving on: : Sunday, December 4, 2016 - 8:17:32 AM

Identifiers

  • HAL Id : dumas-00636806, version 1

Citation

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⟩

Share

Metrics

Record views

180

Files downloads

346