Skip to Main content Skip to Navigation

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.
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download
Contributor : Yann Salmon <>
Submitted on : Monday, May 27, 2013 - 3:39:59 PM
Last modification on : Thursday, January 7, 2021 - 4:25:07 PM
Long-term archiving on: : Tuesday, April 4, 2017 - 11:29:16 AM


Files produced by the author(s)


  • HAL Id : hal-00780124, version 2


Thomas Genet, Yann Salmon. Tree Automata Completion for Static Analysis of Functional Programs. 2013. ⟨hal-00780124v2⟩



Record views


Files downloads