| Analyse d'atteignabilité pour les programmes fonctionnels avec stratégie d'évaluation en profondeur (Reachability analysis for functional programs with innermost evaluation strategy) Salmon, Yann - (2015-12-07) / Université de Rennes 1 - Analyse d'atteignabilité pour les programmes fonctionnels avec stratégie d'évaluation en profondeur
| |||
Langue : Français Directeur(s) de thèse: Genet, Thomas Discipline : Informatique Laboratoire : IRISA Ecole Doctorale : Mathématiques, informatique, signal, électronique et télécommunications Classification : Informatique Mots-clés : programme, preuve, analyse, vérification, OCaml, réécriture, automate, complétion, stratégie, innermost
| |||
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). Abstract : Proving that programs behave correctly is difficult; one uses proof tools, which must rely on overapproximation (because of Rice's theorem). Automaton completion is such a tool, which overapproximates the set of reachable terms during the execution of a program represented as a TRS. An evaluation strategy dictates which subterm of a term should be rewritten first; taking this into account allows for a better approximation. Our thesis sets forward an adaptation of automaton completion to the innermost strategy, which is used among others by OCaml. We prove the soundness and the precision of our adaptation and show how it is part of a greater framework for analysis of functional programms (OCaml). | |||