Skip to Main content Skip to Navigation
Reports

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
Complete list of metadatas

Cited literature [26 references]  Display  Hide  Download

https://hal.inria.fr/hal-00921814
Contributor : Thomas Genet <>
Submitted on : Saturday, December 21, 2013 - 5:49:52 PM
Last modification on : Friday, July 10, 2020 - 4:25:41 PM
Long-term archiving on: : Monday, March 24, 2014 - 9:16:41 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

1378

Files downloads

224