Université de Rennes 1 Analyse d'atteignabilité pour les programmes fonctionnels avec stratégie d'évaluation en profondeur Reachability analysis for functional programs with innermost evaluation strategy programmepreuveanalysevérificationOCamlréécritureautomatecomplétionstratégieinnermost Logiciels -- Vérification É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). 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). Electronic Thesis or DissertationText fr application/tar1 : 646 Kohttps://ecm.univ-rennes1.fr/nuxeo/site/esupversions/e6bf5e35-0346-4183-9ec3-34a03aa79578 Salmon Yann 1987-07-30 FR 192194437 recherche@pro.yannsalmon.fr 2015REN1S085 http://www.theses.fr/2015REN1S085 2015-12-07 Informatique Université de Rennes 1thesis.degree.grantor_1 02778715X Doctorat non ouiGenetThomasintervenant_1140601007 Mathématiques, informatique, signal, électronique et télécommunicationsecoleDoctorale_1 139007164 Université européenne de BretagnepartenaireRecherche_1 139075119 IRISApartenaireRecherche_2 026386909 ddc:004 GenetThomasUniversité de Rennes 1Sciences et technologie, médecine, pharmacie, odontologie, droit, économie, gestion, philosophieMathématiques, informatique, signal, électronique et télécommunicationsÉcole doctorale Mathématiques, informatique, signal, électronique et télécommunications (Rennes)Université européenne de Bretagne Pôle de recherche et d'enseignement supérieur de Bretagne IRISA ASCII PDF 661801