Auto-active Verification of Graph Algorithms, Written in OCaml

TL;DR

This paper demonstrates the successful application of auto-active deductive verification to large-scale, real-world OCaml graph algorithms, showcasing mostly-automated proofs using SMT solvers and the Why3 framework.

Contribution

It introduces the first mostly-automated, mechanized verification of OCaml graph algorithms using Cameleer and SMT solvers, bridging a gap in formal certification of functional programs.

Findings

Most proofs completed automatically with SMT solvers

Verification applied to large-scale OCaml graph algorithms

First mechanized proofs of OCaml graph algorithms

Abstract

Functional programming offers the perfect ground for building correct-by-construction software. Languages of such paradigm normally feature state-of-the-art type systems, good abstraction mechanisms, and well-defined execution models. We claim that all of these make software written in a functional language excellent targets for formal certification. Yet, somehow surprising, techniques such as deductive verification have been seldom applied to large-scale programs, written in mainstream functional languages. In this paper, we wish to address this situation and present the auto-active proof of realistic OCaml implementations. We choose implementations issued from the OCamlgraph library as our target, since this is both a large-scale and widely-used piece of OCaml code. We use Cameleer, a recently proposed tool for the deductive verification of OCaml programs, to conduct the proofs of the selected case studies. The vast majority of such proofs are completed fully-automatically, using SMT solvers, and when needed we can apply lightweight interactive proof inside the Why3 IDE (Cameleer translates an input program into an equivalent WhyML one, the language of the Why3 verification framework). To the best of our knowledge, these are the first mechanized, mostly-automated proofs of graph algorithms written in OCaml.