Vous pouvez vous abonner à nos annonces de séminaires
                     http://gallium.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

                            Lundi 2 avril, 10h30

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

                                    LRI

                ===========================================
                Cubicle: A Parallel SMT-based Model Checker
                         for Parameterized Systems
                ===========================================

Cubicle is a new model checker for verifying safety properties of array-based
systems, a syntactically restricted class of parametrized transition systems
with states represented as arrays indexed by an arbitrary number of
processes. Cache coherence protocols and mutual exclusion algorithms are
typical examples of such systems. Cubicle implements a parallel symbolic
backward reachability procedure using Satisfiabilty Modulo Theories. Its SMT
solver is a tightly integrated, lightweight and enhanced version of Alt-Ergo
and its parallel implementation relies on the Functory library.