We present the formal verification of a subset of the Set module from the OCaml standard library. The proof is conducted using Cameleer, a new tool for the deductive verification of OCaml code. Cameleer takes as input an OCaml program, annotated using the GOSPEL specification language, and translates it into an equivalent program writen in WhyML, the specification and programming language of the Why3 verification framework. We present our verification effort and detail on the main challenges.

Carlos Pinto NOVA LINCS & Universidade da Beira Interior, Portugal

Mário Pereira NOVA LINCS & DI -- Nova School of Science and Technology

Simão Melo de Sousa NOVA LINCS & Universidade da Beira Interior, Portugal