Philippe Regnault (LMR, Université de Reims)

La vérification automatique de systèmes, ou « model checking», est un domaine de l’automatique proposant un certain nombre de techniques pour s’assurer du bon fonctionnement de systèmes automatisés. Le model checking par Monte-Carlo s’inscrit dans cette thématique; il s’agit d’une méthode basée sur la simulation aléatoire d’exécutions du système étudié, visant à explorer en profondeur mais de façon non-exhaustive les différentes routines du système, permettant de s’assurer assez rapidement que le système fonctionne correctement avec probabilité grande.