Le chameau et le serpent rentrent dans un bar : v\'erification quasi-automatique de code OCaml en logique de s\'eparation

TL;DR

This paper introduces a method to translate OCaml programs annotated with Gospel into Viper, enabling automated verification of heap-dependent OCaml code using Separation Logic.

Contribution

It extends Gospel annotations for OCaml to support Separation Logic and implements a translation to Viper for automated verification.

Findings

Successful translation from Gospel-annotated OCaml to Viper

Enhanced verification capabilities for heap-dependent OCaml programs

Extension of Gospel annotations to include Separation Logic features

Abstract

This paper presents a translation from Gospel-annotated OCaml programs into Viper, an intermediate verification language featuring Separation Logic. The practical goal is to extend Cameleer with a new back-end to prove heap-dependent OCaml programs. The logical specification of such OCaml programs is described using an extension of Gospel to support Separation Logic features, which we describe in the paper.