Personnalisation (au choix)

Partie 1:

Introduction à la théorie des jeux pour la vérification et la synthèse. La synthèse de systèmes ouverts ou de contrôleurs part du principe d'un système réactif, qui doit intéragir avec son environnement. Les deux entités - système et environnement - sont vues en tant que 2 joueurs antagonistes. On abordera différents types de jeux : jeux à deux joueurs sur des arènes finies, jeux pour la synthèse de contrôleurs, et jeux distribués.

Partie 2:

Bases théoriques de l'apprentissage par renforcement, un framework de l'intelligence artificielle permettant à des agents d'acquérir des connaissances et de prendre des décisions en interagissant avec leur environnement. Nous explorerons en détail les concepts fondamentaux tels que le problème des bandits manchots, les processus de décision markoviens, les compromis entre exploration et exploitation, le Q-learning, etc. ainsi que des techniques avancées telles que l'approximation de fonction et le Deep Q-learning. À la fin de ce cours, vous aurez entre autres acquis les compétences nécessaires pour comprendre AlphaGo, première IA à surpasser l'humain au jeu de go.

Voir la page complète

Ce cours a pour but principal d’introduire des techniques classiques de vérification et de les implémenter dans un vérificateur de programmes (simples). L’outil réalisé au cours du semestre est capable de détecter des violation d’assertions sur des programmes dans un sous-langage du C (uniquement des entiers et pas de pointeurs) sans que l’utilisateur ait à fournir d’autres information que le programme.

Partie 1:

Cadre général du vérificateur (notamment le langage vérifié et sa sémantique), visant à familiariser avec le langage utilisé (Ocaml) et le SMT-solveur utilisé (Z3), et présentation de la technique du Bounded Model Checking à travers deux algorithmes pour le réaliser.

Partie 2:

Introduction à l'interprétation abstraite, qui consiste à regarder des abstractions de l’ensemble des exécutions d’un programme dans un domaine mathématique bien ordonné plus simple. Durant cette partie, plusieurs domaines abstraits simples sont implémentés.

Partie 3:

Présentation de la technique du raffinement d’abstraction guidé par contre-exemple (CEGAR) et quelques bases sur les réseaux de Petri.

Voir la page complète

L'objectif de cet enseignement est de balayer quelques techniques/approches algorithmiques pour résoudre des problèmes de toutes sortes. Analyser ces techniques pour comprendre pourquoi elles marchent, identifier leurs points forts et leurs faiblesses. Car en algorithmique tout est question de compromis: tel algorithme sera efficace pour telles données ou structures de données. Programmer ces approches et les tester sur un problème en grandeur réelle. Le projet représente 75% de la note finale, 25% pour le test écrit.

Voir la page complète