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

			     S E 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 27 janvier, 10h30

                               ---------------
                               Sylvain Conchon
                               ---------------

                                     LRI

    =====================================================================
    Parameterized Model Checking with a Partial Order Reduction Technique
                        for the TSO Weak Memory Model
    =====================================================================

In this talk, I will present an extended version of the Model Checking Modulo
Theories (MCMT) framework for verifying parameterized systems under the TSO
weak memory model. Our extension relies on three main ingredients: (1) an
axiomatic theory of the TSO memory model based on relations over (read, write)
events, (2) a TSO-specific backward reachability algorithm and (3) an SMT
solver for reasoning about TSO formulas.

One of the main originalities of our work is a partial order reduction
technique that exploits specificities of the TSO memory model. We have
implemented this framework in a new version of the Cubicle model checker
called Cubicle-W. Our experiments show that Cubicle-W is expressive and
efficient enough to automatically prove the safety of concurrent algorithms,
for an arbitrary number of processes, ranging from mutual exclusion to
synchronization barriers translated from actual x86-TSO implementations.