Séminaire Cambium, Inria Paris, 2 rue Simone Iff
                            Salle A215, bâtiment A
                          Lundi 18 septembre, 10h30

                             Arnaud Daby-Seesaram
                                 Inria Paris

                Osiris: an Iris-based program logic for OCaml

Osiris is a project that aims to help OCaml developers verify their
code using Separation Logic. The project is still experimental and
under development. Thus, it supports only a subset of the features of
the OCaml language at the moment. Ultimately, we would like to extend
Osiris to support most features of the language.

Our program logic is based on the Iris framework, which is widely used
to write proofs of programs as it provides expressive ghost state and
several useful builtin proofs techniques. Among other things, these
techniques allow users to reason about potentially divergent programs
and programs manipulating a heap and higher-order functions.

In this talk, I will be giving a live demo of Osiris to prove a small
OCaml program. I will also explain how the tool works by describing
its structure and discussing the difficulties we encountered during
its development.

            Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct:
                     https://bbb.inria.fr/pot-xb8-cq4-y6w