Séminaire Cambium, Inria Paris, 2 rue Simone Iff
                          Salle Lions 1, bâtiment C
                           Lundi 16 janvier, 10h30

                                Léon Gondelman
                              Aarhus University

            Verifying Reliable Network Components in a Distributed
             Separation Logic with Dependent Separation Protocols

In this talk we will take a look on a foundationally verified implementation
of a reliable communication library for asynchronous client-server
communication, and a stack of formally verified components on top thereof. The
library is implemented in OCaml on top of UDP and features characteristic
traits of existing communication protocols, such as a simple handshaking
protocol, bidirectional channels, and retransmission/acknowledgement
mechanisms. We will see how this library is specified in the Aneris
distributed separation logic using a distributed variant of so-called
dependent separation protocols, which hitherto have only been used in a
non-distributed concurrent setting. To verify OCaml programs, we have
implemented a simple compiler that translates programs written in a subset of
OCaml to AnerisLang, the formally defined programming language that Aneris is
proved sound for. I will talk briefly about this translation and then show how
that specification of the reliable communication library simplifies formal
reasoning about applications, such as a remote procedure call library, which
in turn is used to verify a lazily replicated key-value store with
leader-followers and some clients thereof. Importantly, the development is
highly modular -- each component is verified relative to specifications of the
components it uses (not the implementation).

            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://webconf.math.cnrs.fr/b/fra-ryy-fjn