HASLab

7/24/2017

By Mário Pereira, LRI — Université Paris-Saclay, France.

Abstract. Programming libraries are the basic building blocks of any realistic programming project. It is then of most interest for a programmer to build her software on top of bug-free libraries. Even massively used and tested libraries can contain bugs: in 2006 a bug was found in the Java’s standard library, after 9 years of undetected presence. One possibility to verify the behavior of such libraries is to employ deductive software verification, that is the idea of breaking down the correctness of a program into a mathematical statement and then proving it. Projects such as CompCert and seL4 show how proof assistants can handle large program verification efforts. In addition, the remarkable improvement on SMT solvers make it possible to apply these tools to the verification of real- istic program artifacts. For instance, the Verisoft XT project was verified using VCC, which builds on the SMT solver Z3. It may come as a surprise, but program verification has been very little applied to libraries of significant size. A remarkable exception is the verification of the EiffelBase2 containers library, performed with the AutoProof system.

This work presents the first steps towards VOCAL, a mechanically verified library of efficient general-purpose data structures and algorithms, written in the OCaml language. OCaml is the implementation language of worldwide used systems where stability, safety, and correctness are of utmost importance. Examples include the Coq proof assistant, the Astrée and Frama-C static analyzers, the Cubicle model-checker, and the Alt-Ergo theorem prover. Such tools would immediately benefit from a verified OCaml library. In the VOCAL project, we use a combination of three tools to tackle the formal development of the library: CFML, Coq, and Why3. In this talk we focus on the use of Why3 to verify some of VOCAL’s modules. Starting from a formally specified OCaml signature file (we use a new specification language for the OCaml language, currently under development) we generate a correspondent signature on the Why3 side. We then write a verified implementation of this signature, and use a new refinement mechanism to show that the implementation indeed respects the signature. Finally, we use Why3’s code extraction mechanism to obtain correct-by-construction OCaml code.

Keywords. Deductive verification, Why3, OCaml, library, code extraction, refinement, iteration, specification language

About the Speaker. Mário Pereira is currently a 3rd year PhD candidate at Université Paris-Saclay, France, and researcher at LRI (Laboratoire de Recherche en Informatique), France, working within 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 on ``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, program transformations. Mário is the winner of the software competition VerifyThis in 2016 and 2017 editions. Mário is currently a main developers of the Why3 verification platform and the main developer of the VOCAL library, a mechanically verified OCaml library, whose first release will appear soon. You can learn more about the speaker here: https://www.lri.fr/~mpereira/.