Towards Static Analysis of Functional Programs using Tree Automata Completion

Thomas Genet 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : This paper presents the first step of a wider research effort to apply tree automata completion to the static analysis of functional programs. Tree Automata Completion is a family of techniques for computing or approximating the set of terms reachable by a rewriting relation. The completion algorithm we focus on is parameterized by a set $E$ of equations controlling the precision of the approximation and influencing its termination. For completion to be used as a static analysis, the first step is to guarantee its termination. In this work, we thus give a sufficient condition on $E$ and $\TF$ for completion algorithm to always terminate. In the particular setting of functional programs, this condition can be relaxed into a condition on $E$ and $\TC$ (terms built on the set of constructors) that is closer to what is done in the field of static analysis, where abstractions are performed on data.
Type de document :
[Research Report] 2013, pp.15
Liste complète des métadonnées

Littérature citée [26 références]  Voir  Masquer  Télécharger
Contributeur : Thomas Genet <>
Soumis le : samedi 21 décembre 2013 - 17:49:52
Dernière modification le : vendredi 16 novembre 2018 - 01:38:53
Document(s) archivé(s) le : lundi 24 mars 2014 - 09:16:41


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-00921814, version 1


Thomas Genet. Towards Static Analysis of Functional Programs using Tree Automata Completion. [Research Report] 2013, pp.15. 〈hal-00921814〉



Consultations de la notice


Téléchargements de fichiers