Logo IRISA logo Inria

Prochain Exposé

Vendredi 21 juin, 14h30 en salle MARKOV

Sylvain Conchon

Vérification de systèmes paramétrés avec Cubicle

Dans cet exposé, je présenterai Cubicle, un model checker conçu pour vérifier des propriétés de sûreté sur des systèmes à tableaux. Il s’agit d’une classe restreinte de systèmes paramétrés dont les états sont représentés par des tableaux indexés par un nombre arbitraire d’identificateurs de processus. Les protocoles de cohérence de cache ou les algorithmes d’exclusion mutuelle sont des exemples typiques de tels systèmes. Cubicle implémente une technique de model checking appelée MCMT (Model Checking Modulo Theories). Cette technique repose sur un algorithme d’atteignabilité arrière symbolique couplé à un démonstrateur automatique SMT (Satisfiability Modulo Theories). Je présenterai également nos derniers développements sur une extension de Cubicle pour vérifier des systèmes avec des mémoires faibles.

Exposés des semaines suivantes

Jeudi 27 juin, 14h00 en salle Minquier

Djamel Eddine Khelladi

TBA

TBA

Vos propositions sont les bienvenues !

Séminaire autour des thèmes 68NQRT