Static analyzers have been successfully developed to detect runtime errors in many languages. However, the automatic analysis of functional languages remains a challenge due to their systematic use of recursion, algebraic data types, and higher-order functions. Compiler-integrated 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 program invariants.
This thesis aims at designing a static value analysis by abstract interpretation for a higher-order pure functional language. This analysis provides a sound and automatic approach to discover invariants and prevent assertion and match failures. We have designed a bottom-up compositional analysis: functions are analyzed only once, at their definition site, generating a summary of their behavior. We aim at generating precise summaries, proving expressive properties on functions. To do so, we developed a relational domain for recursive algebraic data types and we formalized disjunctive relational summaries to abstract higher-order functions. To improve the precision of those summaries, we developed a language-agnostic relational domain on containers. Our analysis is implemented in the platform MOPSA for a pure subset of OCaml.