Orateurices

Damien BUSATTO-GASTON

Titre : Vérification de modèles stochastiques et synthèse de contrôleurs à spécifications probabilistes.

Ce cours présente des résultats de vérification de modèles.  Un système, que l'on assimile à l'ensemble de ses exécutions possibles, est comparé à une spécification, c'est-à-dire une propriété attendue des exécutions du système.  Au lieu de chercher à garantir un degré d'exactitude absolu -- "toutes les exécutions ont la propriété voulue" -- on présentera des modèles et des spécifications comportant des aspects probabilistes.  On pourra alors exprimer des propriétés telles que "la spécification est satisfaite la plupart du temps", ou encore "la probabilité d'échec est inférieure à 0.1%".  On mènera donc une analyse formelle de systèmes comportant des aspects probabilistes, représentés par une chaîne de Markov ou un processus de décision markovien (MDP).  Le domaine d'application est varié. Il inclut la modélisation d'algorithmes probabilistes ou encore l'expression de garanties formelles en présence d'incertitudes liées à un environnement extérieur -- par exemple, la possibilité que des messages se perdent dans un protocole de communication. 

-----

Christine TASSON et Guillaume BAUDART

Titre : Introduction à la programmation probabiliste.

La programmation probabiliste est un paradigme qui a connu un essor important ces dernières années. 
Les langages probabilistes manipulent l'incertitude de manière explicite. Ils reposent sur la méthode Bayésienne qui permet d'apprendre la distribution des paramètres d'un modèle a partir d'observations statistiques.
De nombreux langages de programmation ont été développés e.g., WebPPL, Venture, Anglican, Stan, Gen, Pyro, Turing.jl... Ces langages sont utilisés dans des domaines qui vont de la vision (génération d'images) et la robotique (planification), à la santé (épidémiologie) et les sciences sociales (sondages).
 
Ce cours présente les concept fondamentaux de la programmation probabiliste :
- Introduction à la modélisation Bayésienne
- Conception d'un langage probabiliste et d'un moteur d'inférence
- Sémantiques formelles pour raisonner sur les programmes probabilistes

-----

Mathilde BOUVEL

Titre : Combinatoire symbolique (et analytique), séries génératrices bivariées, et distribution de paramètres sur des objets discrets

Dans ce mini-cours, on montre comment décomposer les objets discrets au moyen de spécifications combinatoires, et comment celles-ci peuvent être traduites en équations pour les séries génératrices d'énumération des objets considérés. Puis on introduit des raffinements bivariés de ces séries, afin d'étudier le comportement de paramètres sur nos objets discrets. On explique comment ces séries bivariées permettent d'avoir accès à la moyenne, ou même à la distribution, du paramètre considéré.  Ceci permet de mieux comprendre nos objets d'étude, notamment lorsque leur taille tend vers l'infini. Ce mini-cours est illustré de nombreux exemples.

-----

Romain AZAÏS

Titre : Construction d'estimateurs pour les processus markoviens déterministes par morceaux en biologie

Un processus de Markov déterministe par morceaux est un processus stochastique à temps continu, évoluant de manière déterministe à presque chaque instant, mais subissant ponctuellement des perturbations aléatoires à des instants aléatoires. Cette classe de processus permet de modéliser une grande variété de phénomènes biologiques, des suites de croissance et division des cellules à des expositions à un contaminant alimentaire. A partir d'observations en temps long, on montrera comment construire des estimateurs des caractéristiques du processus ainsi que de quantités d'intérêt liées au dépassement d'un seuil critique.

-----

Marine MINIER

Titre : Outils automatiques pour la résolution de problèmes de cryptanalyse en cryptographie symétrique.

Le but de cette présentation est de montrer les problèmes posés par la modélisation d'une attaque différentielle sur un chiffrement par bloc donné.Le principal obstacle réside dans la difficulté de modéliser correctement l'opérateur XOR qui augmente la taille de l'arbre de recherche. Pour cela, nous utiliserons d'abord le langage de haut niveau Minizinc et un solveur SAT ou MILP puis le langage de programmation par contraintes écrit en Java, Choco.