Résultat majeur : CUBICLE: A PARALLEL SMT-BASED MODEL CHECKER FOR PARAMETERIZED SYSTEMS
CUBICLE: A PARALLEL SMT-BASED MODEL CHECKER FOR PARAMETERIZED SYSTEMS 22 mars 2012
Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout, Fatiha Zaïdi, CAV 2012
Cubicle is a new model checker for verifying safety properties of
parameterized systems. It implements a parallel symbolic backward reachability procedure using Satisfiabilty Modulo Theories. Experiments done on classic and challenging mutual exclusion algorithms and cache coherence protocols show
that Cubicle is effective and competitive with state-of-the-art model checkers.
Cubicle is available at http://cubicle.lri.fr
