Séminaire Cambium, Inria Paris, 2 rue Simone Iff Salle A215, bâtiment A Lundi 28 novembre, 10h30 Alexandre Moine Inria Paris A High-Level Separation Logic for Heap Space under Garbage Collection A garbage collector greatly simplifies the life of a programmer: it automates the tedious task of deallocating memory. However, the heap space usage of garbage collected programs can be tricky to understand and reason about, as there is no explicit program point where space is reclaimed. Last year, Madiot & Pottier presented a Separation Logic with Space Credits to reason about heap space under garbage collection. They introduce pointed-by assertions to keep track of the predecessors of every block, and to prove that a block is unreachable. However, their work is carried out in the setting of an assembly-like programming language. In this talk, we scale up to a high-level language, where a central problem is to identify the memory locations that the garbage collector considers as roots. For this purpose, we propose new "Stackable" assertions, which keep track of the existence of stack-to-heap pointers in a reasonably lightweight manner. In addition, we explain how to reason about function closures, which involve heap-allocated blocks that may hold pointers onto other blocks. 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