Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Practical Deductive Verification of OCaml Programs (Extended Version)

Mário Pereira

TL;DR

The paper presents a practical, tutorial-style approach to deductive verification of OCaml programs using GOSPEL and the Cameleer tool, demonstrating a pipeline that translates annotated OCaml into WhyML for Why3-based verification with SMT solvers. It targets both purely functional programs and imperative code with mutable state and exceptions, illustrating modular verification with OCaml functors through two representative case studies: a functional merge routine and a linear array search, then extending to a purely functional tree comparison (same fringe) and an imperative Boyer-Moore MJRTY algorithm. Key contributions include a concrete workflow that combines GOSPEL specifications, modular design via functors, and a spectrum of proofs (including lemmas and invariants) that enable automation, as well as a discussion of verification challenges and debugging within the Why3/Reasoning environment. The work underscores the practicality of making formal methods accessible to regular OCaml programmers, highlights the role of lemmas for automation, and provides an artifact with additional case studies, paving the way for broader adoption of deductive verification in real-world OCaml development with tool-assisted guarantees.

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.

Practical Deductive Verification of OCaml Programs (Extended Version)

TL;DR

The paper presents a practical, tutorial-style approach to deductive verification of OCaml programs using GOSPEL and the Cameleer tool, demonstrating a pipeline that translates annotated OCaml into WhyML for Why3-based verification with SMT solvers. It targets both purely functional programs and imperative code with mutable state and exceptions, illustrating modular verification with OCaml functors through two representative case studies: a functional merge routine and a linear array search, then extending to a purely functional tree comparison (same fringe) and an imperative Boyer-Moore MJRTY algorithm. Key contributions include a concrete workflow that combines GOSPEL specifications, modular design via functors, and a spectrum of proofs (including lemmas and invariants) that enable automation, as well as a discussion of verification challenges and debugging within the Why3/Reasoning environment. The work underscores the practicality of making formal methods accessible to regular OCaml programmers, highlights the role of lemmas for automation, and provides an artifact with additional case studies, paving the way for broader adoption of deductive verification in real-world OCaml development with tool-assisted guarantees.

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.
Paper Structure (25 sections, 6 figures)

This paper contains 25 sections, 6 figures.

Table of Contents

  1. Introduction
  2. A Primer on GOSPEL
  3. The Cameleer Verification Tool
  4. A Simple Functional Program -- the Merge Routine
  5. Modular Definitions, Using Functors.
  6. OCaml Implementation.
  7. GOSPEL Specification.
  8. Cameleer Proof.
  9. Searching an Element Within an Array
  10. OCaml Implementation.
  11. Cameleer Proof.
  12. Providing an Incorrect Loop Invariant.
  13. Purely Functional Programming
  14. Same Fringe -- Comparing Two Binary Trees
  15. Summary
  16. ...and 10 more sections

Figures (6)

  • Figure 1: GOSPEL-annotated Stack Interface.
  • Figure 2: Cameleer Architecture and verification pipeline, taken from pereira2021cameleer.
  • Figure 3: Type Equipped With a Total Preorder Relation.
  • Figure 4: Why3 Proof Session for the Merge Sort Routine.
  • Figure 5: Type Equipped With an Equality Relation.
  • ...and 1 more figures