Séminaire Cambium, Inria Paris
                                     BJ09
                            Vendredi 7 mars, 10h30

                                Clément Allain
                                 Inria Paris

                   Zoo: A framework for the verification of
              concurrent OCaml 5 programs using separation logic

The release of OCaml 5, which introduced parallelism into the
language, drove the need for safe and efficient concurrent data
structures. New libraries like Saturn aim at addressing this need.
From the perspective of formal verification, this is an opportunity to
apply and further state-of-the-art techniques to provide stronger
guarantees.

We present a framework for verifying fine-grained concurrent OCaml 5
algorithms. Following a pragmatic approach, we support a limited but
sufficient fragment of the language whose semantics has been carefully
formalized to faithfully express such algorithms. Source programs are
translated to a deeply-embedded language living inside Rocq where they
can be specified and verified using the Iris concurrent separation
logic.

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

             Nos séminaires sont accessibles en ligne en direct
                            via le lien ci-dessus.