Detail

VOCaL – The Verified OCaml Library

Libraries are the basic building blocks of any realistic programming project. It is thus of utmost interest for a programmer to build her software on top of bug-free libraries. Although this may seem surprising, program verification has seldom been applied to libraries of significant size. We present the ongoing VOCaL project, which aims at building a mechanically verified library of general-purpose data structures and algorithms, written in the OCaml language.

One of the key ingredients of the VOCaL project is the design of a new specification language for OCaml, independently of any verification tool. This is similar to what JML is for Java, or
ACSL for C. Another ingredient of the VOCaL project is the development of the verified library itself, using a combination of three tools: CFML, Coq, and Why3. In this talk we present the
current state of the specification language and the library itself. We will focus particularly on the use of the Why3 tool and, using a running example, we will show how we extended this tool in the scope of the VOCaL project: an enhanced extraction mechanism featuring a modular translation, up to OCaml functors; a new refinement mechanism; a tool to translate annotated .mli files to WhyML, the language of Why3; a systematic way to build memory models for strongly imperative OCaml programs. We will conclude by presenting the already verified OCaml modules and how we successfully coped with technical challenges such as modular
proofs, absence of arithmetic overflow, unverified clients and iteration.