Jean-Christophe Filliâtre

Lab. de Recherche en Informatique, Univ. Paris-Sud, CNRS, France

Deductive Verification of OCaml Libraries

In this talk, we report on an on-going project, VOCaL, which aims at building formally-verified general-purpose OCaml libraries of data structures and algorithms. We present the various ingredients of this project. First, we introduce GOSPEL, a specification language for OCaml. It resembles existing behavioral specification languages (e.g. JML, ACSL, SPARK), yet departs from them on several points. Second, we describe techniques and tools to perform deductive verification of GOSPEL-specified OCaml code. Currently, this is built on top of three existing tools, namely Why3, CFML and Coq. Last, we report of the successful verification of the first OCaml modules of the VOCaL library. This includes general-purpose data structures such as resizable arrays, hash tables, priority queues, and union-find.

Jean-Christophe Filliâtre is a senior researcher at CNRS. He works at University Paris Sud in Orsay, France. He is chair of IFIP working group 1.9/ 2.15 “Verified Software”. His Ph.D. (1999) was related to the verification of imperative programs using interpretations in type theory, within the framework of the Coq proof assistant. It soon evolved into a tool of its own, known as Why3, where deductive program verification can be performed with the help of many off-the-shelf theorem provers. Jean-Christophe Filliâtre has been working on Why3 since 2001.