9h-9h30 Accueil, café
9h30-10h Emmanuel Haucourt (CEA-X, Saclay)
Titre : Geometric models for concurrency (the so called swiss flag)
Abstract:
Survol de quelques modèles topologiques de la concurrence et présentationde l'outil ALCOOL. Ensembles cubiques, cylindriques et toriques. Présentation des directions de recherche privilégiées.
10h-10h15 Pause
10h15-10h45 Jules Villard (LSV, Cachan)
Titre : Proving Copyless Message Passing
Abstract:
Handling concurrency using a shared memory and locks is tedious and
error-prone. One solution is to use message passing instead. We study
here a particular, contract-based flavor that makes the ownership
transfer of messages explicit. In this case, ownership of the heap
region representing the content of a message is lost upon sending, which
can lead to efficient implementations. In this talk, we define a proof
system for a concurrent imperative programming language implementing
this idea and inspired by the Singularity OS. The proof system is an
extension of separation logic, which has already been used successfully
to study various ownership-oriented paradigms. A fragment of it is
automatized in a tool, Heap-Hop.
Slides
10h45-11h Pause
11h-11h30 Emanuel Godard (LIF, Marseille)
Titre : Topological techniques for distributed algorithms: the case of the coordinated attack problem.
Abstract:
TBA
11h30-11h45 Pause
11h45-12h15 David
Baelde (Parsifal, LiX, Palaiseau)
Titre : TBA
Abstract:
12h15-13h45 Déjeuner
14h-14h30 Samy Abbes (PPS, Paris) Titre : TBA
Abstract:
14h30-16h Conclusion-Discussion
14h30-16h Conclusion-Discussion
