Tree Automata Completion for Static Analysis of Functional Programs

Thomas Genet 1 Yann Salmon 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
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


https://hal.archives-ouvertes.fr/hal-00780124
Contributeur : Yann Salmon <>
Soumis le : lundi 27 mai 2013 - 15:39:59
Dernière modification le : jeudi 9 février 2017 - 15:34:55
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

812

Téléchargements du document

168