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.
13/07/2018 13:30
Software Systems
Mário Pereira is currently a last year PhD candidate at Université Paris-Saclay, France, and researcher at LRI (Laboratoire de Recherche en Informatique), France, working within the Why3 team, under the supervision of Jean-Christophe Filliâtre. Mário got his BSc engineering degree from Universidade da Beira Interior (ranked 1st) and MSc degree (major in logic and computation) from FCUP, Porto (ranked 1st). Mário's research interests are mainly deductive software verification, functional programming, type systems, module systems, and program transformations. Mário is the winner of the software competition VerifyThis in 2016 and 2017 editions. Mário is currently one of the main developers of the Why3 verification platform, as well as of the VOCAL library, a mechanically verified OCaml library, whose first release will appear soon.
