To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 11/05/07 - Paris - FR

           Vous pouvez vous abonner à nos annonces de séminaires
                    http://pauillac.inria.fr/seminaires/

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                         Amphi Turing du bâtiment 1

                           Vendredi 11 mai, 10h30

                              ----------------
                              Viktor Vafeiadis
                              ----------------

                          University of Cambridge

             =================================================
             A marriage of rely/guarantee and separation logic
             =================================================

Verifying concurrent programs is difficult because the proof must
consider the interactions between the threads. Fine-grain concurrency
and heap allocated data structures exacerbate this problem, because
threads interfere more often and in richer ways.

I will present a new logic, RGSep, that is well-suited for proving
pointer-manipulating fine-grain concurrent algorithms. RGSep permits
natural interference to be described naturally (using a relation as in
rely/guarantee), and where there is no interference, it enables local
reasoning (as in separation logic).  I will demonstrate its usefulness
with a prototype tool that proves the correctness of a number of
concurrent list algorithms, some of which actually dispose (free)
deleted nodes.