Tree Automata Completion for Static Analysis of Functional Programs

Thomas Genet 1 Yann Salmon 1
1 CELTIQUE - Software certification with semantic analysis
IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL, Inria Rennes – Bretagne Atlantique
Abstract : Tree Automata Completion is a family of techniques for computing or approximating the set of terms reachable by a rewriting relation. For functional programs translated into TRS, we give a sufficient condition for completion to terminate. Second, in order to take into account the evaluation strategy of functional programs, we show how to refine completion to approximate reachable terms for a rewriting relation controlled by a strategy. In this paper, we focus on innermost strategy which represents the call-by-value evaluation strategy.
Liste complète des métadonnées

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

https://hal.archives-ouvertes.fr/hal-00780124
Contributeur : Yann Salmon <>
Soumis le : lundi 27 mai 2013 - 15:39:59
Dernière modification le : mercredi 2 août 2017 - 10:09:46
Document(s) archivé(s) le : mardi 4 avril 2017 - 11:29:16

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00780124, version 2

Citation

Thomas Genet, Yann Salmon. Tree Automata Completion for Static Analysis of Functional Programs. 2013. 〈hal-00780124v2〉

Partager

Métriques

Consultations de la notice

885

Téléchargements de fichiers

177