Analyse d’atteignabilité pour les programmes fonctionnels avec stratégie d’évaluation en profondeur

Yann Salmon 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Résumé : Établir des preuves de bon fonctionnement des programmes est délicat ; on a recours à des outils de preuve, qui doivent procéder par surapproximation (à cause du théorème de Rice). La complétion d'automate est un tel outil, qui surapproxime l'ensemble des termes accessibles lors de l'exécution d'un programme représenté par un système de réécriture. La stratégie d'évaluation donne l'ordre dans lequel les sous-termes d'un terme doivent être réécrits ; en tenir compte permet une meilleur précision de l'analyse. Notre thèse propose une adaptation de la complétion d'automate à la stratégie en profondeur, utilisée notamment par OCaml. Nous établissons la correction et la précision de notre méthode et montrons comment elle s'inscrit dans le cadre plus large de l'analyse de programmes fonctionnels (OCaml).
Type de document :
Thèse
Théorie et langage formel [cs.FL]. Université de Rennes 1, 2015. Français. 〈NNT : 2015REN1S085〉
Liste complète des métadonnées

Littérature citée [44 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/tel-01250252
Contributeur : Thomas Genet <>
Soumis le : lundi 21 mars 2016 - 09:43:17
Dernière modification le : mercredi 16 mai 2018 - 11:23:28
Document(s) archivé(s) le : mercredi 22 juin 2016 - 10:47:42

Licence


Copyright (Tous droits réservés)

Identifiants

  • HAL Id : tel-01250252, version 2

Citation

Yann Salmon. Analyse d’atteignabilité pour les programmes fonctionnels avec stratégie d’évaluation en profondeur. Théorie et langage formel [cs.FL]. Université de Rennes 1, 2015. Français. 〈NNT : 2015REN1S085〉. 〈tel-01250252v2〉

Partager

Métriques

Consultations de la notice

474

Téléchargements de fichiers

180