en fr Reachability Analysis for Functional Programs with call-by-value evaluation strategy Analyse d’atteignabilité pour les programmes fonctionnels avec stratégie d’évaluation en profondeur Reportar como inadecuado




en fr Reachability Analysis for Functional Programs with call-by-value evaluation strategy Analyse d’atteignabilité pour les programmes fonctionnels avec stratégie d’évaluation en profondeur - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 CELTIQUE - Software certification with semantic analysis Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL

Abstract : This document presents an extension of tree automata completion to innermost rewriting.


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.


en fr

Keywords : innermost strategy tree automata Term Rewriting reachability analysis

Mots-clés : analyse d-atteignabilité Réécriture automates d-arbres stratégie d-évaluation en profondeur





Autor: Yann Salmon -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados