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 :
Rapport
[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

https://hal.inria.fr/hal-00921814
Contributeur : Thomas Genet <>
Soumis le : samedi 21 décembre 2013 - 17:49:52
Dernière modification le : mercredi 16 mai 2018 - 11:23:28
Document(s) archivé(s) le : lundi 24 mars 2014 - 09:16:41

Fichier

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

Identifiants

  • HAL Id : hal-00921814, version 1

Citation

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

Partager

Métriques

Consultations de la notice

1013

Téléchargements de fichiers

116