Le chameau et le serpent rentrent dans un bar : vérification quasi-automatique de code OCaml en logique de séparation

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.

in French language