Reachability Analysis of Innermost Rewriting

International audienceWe consider the problem of inferring a grammar describing the output of a functional programgiven a grammar describing its input. Solutions to this problem are helpful for detecting bugs orproving safety properties of functional programs and, several rewriting tools exist for solving thisproblem. However, known grammar inference techniques are not able to take evaluation strategiesof the program into account. This yields very imprecise results when the evaluation strategymatters. In this work, we adapt the Tree Automata Completion algorithm to approximateaccurately the set of terms reachable by rewriting under the innermost strategy. We prove thatthe proposed technique is sound and precise w.r.t. innermost rewriting. The proposed algorithmhas been implemented in the Timbuk reachability tool. Experiments show that it noticeablyimproves the accuracy of static analysis for functional programs using the call-by-value evaluation strateg