Functional correctness consists in verifying that a function complies to a given specification. It is often performed by deductive verifiers through annotations and solvers. However, compositional analysis by abstract interpretation can generate function summaries, i.e. contracts valid for every input. Though less expressive than deductive approaches, it discovers function summaries without user-annotations. This approach leverages relational abstract domains to yield a high precision. These automatically generated contracts, in cooperation with deductive verifiers, can discharge some proof obligations and alleviate the annotation burden.

This proposal describes an undergoing line of research in the MOPSA static analysis platform, aiming at developing highly-precise relational domains to automatically infer functional correctness properties. Our analyzer can infer precise summaries for ADT-manipulating OCaml higher-order functions. More expressive domains are under development.