Static and Dynamic Verification of OCaml Programs: The Gospel Ecosystem (Extended Version)

TL;DR

This paper explores the combined use of static and dynamic analysis tools within the Gospel ecosystem to verify OCaml programs, demonstrating their complementary strengths through a detailed case study.

Contribution

It introduces a framework integrating Gospel with Ortac, Cameleer, and CFML for collaborative static and dynamic verification of OCaml code, highlighting their differences and synergies.

Findings

Tools complement each other effectively in verification tasks.

Static and dynamic specifications reveal different insights.

Case study demonstrates practical application of combined analysis.

Abstract

We present our work on the collaborative use of dynamic and static analysis tools for the verification of software written in the OCaml language. We build upon Gospel, a specification language for OCaml that can be used both in dynamic and static analyses. We employ Ortac, for runtime assertion checking, and Cameleer and CFML for the deductive verification of OCaml code. We report on the use of such tools to build a case study of collaborative analysis of a non-trivial OCaml program. This shows how these tools nicely complement each others, while at the same highlights the differences when writing specification targeting dynamic or static analysis methods.