Responsables : Eugene Asarin et Tayssir Touili
Laboratoire : LIAFA, équipe Vérif
Contacts : asarin@liafa.jussieu.fr, touili@liafa.jussieu.fr
Le model-checking régulier est une technique de vérification automatique basée sur l’utilisation des automates comme structures de données. Cette approche a permis, pendant cinq dernières années, de faire un progrès considérable dans la vérification des systèmes infinis et paramétrés.
L'objectif de ce stage consiste à développer les méthodes de model-checking régulier pour les systèmes probabilistes (chaines de Markov définies par des systèmes de réécriture probabiliste). Le stagiaire pourra également implémenter les méthodes développées en prototype d’outil logiciel, et étudier des applications aux systèmes informatiques, physiques et biologiques. Ce sujet nous semble très riche, il y a assez de matière pour en faire ensuite une thèse.
Il est souhaitable d’avoir suivi un cours de vérification (2-8 ou 2-9). Les connaissances de base en probabilités seront également utiles.