Sites Inria

English version

Séminaires des équipes de recherche

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

Séminaire Gallium - Moscova

  • Date : 2/04/2012
  • Lieu : Inria - Rocquencourt - Amphithéâtre Alan Turing
  • Intervenant(s) : Sylvain Conchon - LRI
  • Organisateur(s) : Gallium - Moscova

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.

Mots-clés : Paris - Rocquencourt Séminaire Moscova Gallium

Haut de page

Suivez Inria