|
17-21 juin 2024 Nantes (France)
|
|
|
|
OrateuricesDamien BUSATTO-GASTONTitre : 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 BAUDARTTitre : Introduction à la programmation probabiliste. La programmation probabiliste est un paradigme qui a connu un essor important ces dernières années.
----- Mathilde BOUVELTitre : Combinatoire symbolique (et analytique), séries génératrices bivariées, et distribution de paramètres sur des objets discrets Dans ce 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.
----- Romain AZAÏSTitre : 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 MINIERTitre : 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.
|
| Personnes connectées : 3 | Vie privée |
|
