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.