Practical Deductive Verification of OCaml Programs (Extended Version)

TL;DR

This paper presents a practical approach for deductive verification of OCaml programs using GOSPEL and Cameleer, covering both functional and imperative code with mutable state and complex control flow.

Contribution

It provides a comprehensive tutorial on applying deductive verification to OCaml, demonstrating the use of GOSPEL and Cameleer for mostly-automated verification of functional and imperative programs.

Findings

Effective verification of purely functional OCaml programs.

Verification techniques for imperative OCaml programs with mutable state.

Guidelines for applying deductive verification in practical OCaml development.

Abstract

In this paper, we provide a comprehensive, hands-on tutorial on how to apply deductive verification to programs written in OCaml. In particular, we show how one can use the GOSPEL specification language and the Cameleer tool to conduct mostly-automated verification on OCaml code. In our presentation, we focus on two main classes of programs: first, purely functional programs with no mutable state; then on imperative programs, where one can mix mutable state with subtle control-flow primitives, such as locally-defined exceptions.