Tree Automata Completion for Static Analysis of Functional Programs
Thomas Genet, Salmon, Yann · HAL (Le Centre pour la Communication Scientifique Directe) · 2013
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.