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

			     S É M I N A I R E

                   ______                __    _
                  / ____/___ _____ ___  / /_  (_)_  ______ ___
                 / /   / __ `/ __ `__ \/ __ \/ / / / / __ `__ \
                / /___/ /_/ / / / / / / /_/ / / /_/ / / / / / /
                \____/\__,_/_/ /_/ /_/_.___/_/\__,_/_/ /_/ /_/

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                           Lundi 6 décembre, 10h30

                               ----------------
                               François Pottier
                               ----------------

                                 Inria Paris

          ==========================================================
          A separation logic for heap space under garbage collection
          ==========================================================

We are fond of garbage collection because of the greater simplicity, safety,
and efficiency that it offers, in comparison with explicit manual memory
management. However, reasoning about the space usage of a program, in the
presence of garbage collection, requires some expertise, and can be tricky.
Could this kind of reasoning be performed in the formal setting of a program
logic? What assertions and what reasoning rules would be needed?

In this talk, I will present SL♢, a Separation Logic that allows controlling
the heap space consumption of a program in the presence of dynamic memory
allocation and garbage collection. This logic involves a new kind of resource:
space credits. Space credits are consumed when an object is allocated. They
are produced when a group of objects is logically deallocated, that is, when
the user is able to prove that these objects have become unreachable and
therefore can be collected. To prove such a fact, the user maintains
pointed-by assertions that record the immediate predecessors of every object.

This is joint work with Jean-Marie Madiot.