Skip to Main content Skip to Navigation
New interface
Reports (Research report)

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.
Document type :
Reports (Research report)
Complete list of metadata

Cited literature [26 references]  Display  Hide  Download
Contributor : Thomas Genet Connect in order to contact the contributor
Submitted on : Saturday, December 21, 2013 - 5:49:52 PM
Last modification on : Wednesday, October 26, 2022 - 8:16:22 AM
Long-term archiving on: : Monday, March 24, 2014 - 9:16:41 AM


Files produced by the author(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⟩



Record views


Files downloads