Séminaires des équipes de recherche
Cubicle: A Parallel SMT-based Model Checker for Parameterized Systems
- 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.