Static analyzers have been successfully developed to detect runtime errors in many languages. However, automatic analysis of functional languages remains a challenge, due to their recursive functions, recursive algebraic datatypes and higher order. Classical type systems provide compositional methods that are in general not precise enough to prove the absence of runtime errors such as assertion failures. At the other end of the spectrum, deductive methods are more expressive but may require user guidance to prove invariants.

Our work describes a value static analyzer by abstract interpretation for a higher-order pure functional language, a sound and automatic approach to discover invariants, prevent assertion and match failures. Based on relational abstract domains, our method is able to analyze higher-order recursive functions manipulating algebraic data types by inferring input-output relations. To this end, we introduce a domain summarizing recursive algebraic data-types, which is parameterized by the different abstractions of the underlying types, and lift existing disjunctive relational summaries to higher-order by formalizing them as a domain able to abstract higher-order functions. The resulting analysis is compositional: functions are analyzed once and for all at their definition site, generating a summary of their behavior.

This framework enables a precise and relational abstract interpretation-based analysis for higher-order pure functional languages. This analysis is implemented in the open-source multi-language platform MOPSA, for a subset of OCaml. Preliminary evaluation confirms the precision of our approach on a set of 40 handwritten toy programs and 20 programs from state-of-the-art Salto analyzer.