Semestre 9 - Algorithmes et méthodes formelles (AMF)

Voir la page complète

Majeure en algorithmique avancée, mineure en vérification logicielle

Voir la page complète

Voir la page complète

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

Ce cours introduit la logique des modèles finis, tels que les mots, les arbres et les graphes fini, ainsi que des logiques temporelles utilisées en vérification. Nous présenterons également les logiques de description qui servent à représenter de manière formelle des connaissances d’un domaine particulier (e.g. médecine) pour améliorer l’interrogation et le partage d'informations. On s’intéressera au pouvoir d’expression des logiques considérées, ainsi que des problèmes algorithmiques variés (validation de formule sur un modèle, satisfiabilité de formule, inférence logique, etc).

Nous aborderons également l’apprentissage d'automates et de formules LTL à partir d’exemples dans des contextes passifs et actifs. Nous discuterons des algorithmes associés à ces problèmes (bornes supérieures) ainsi que des questions de complexité (bornes inférieures). Si le temps le permet, nous mettrons également en lumière un lien étroit entre la théorie des automates et la complexité des circuits algébriques, et montrerons comment les résultats de l'une peuvent être appliqués à l'autre.

Voir la page complète

La théorie des graphes est un modèle très général qui permet de représenter des problèmatiques très variées, que ce soit dans les réseaux (de toute nature) mais aussi pour des structures hierarchisées comme les bases de données. La culture générale des problématiques de graphe que nous proposons dans ce cours ainsi que la connaissance des outils efficaces pour ces problématiques sont des atouts pour reconnaître et traiter les problèmes qu'elles modélisent.

Cet enseignement présente des notions avancées de théorie des graphes et familiarise l’étudiant avec certaines techniques de preuve classiques, liées notamment à la coloration de graphes. Quelques problèmes et conjectures classiques sont abordés.

Voir la page complète

Objectifs : introduire l’algorithmique distribuée; présenter les différents modèles et contraintes du calcul distribué ; présenter et analyser quelques algorithmiques classiques du domaine ; concevoir des algorithmes s'exécutant sur des systèmes distribués

Voir la page complète

Le but de ce cours est de familiariser les étudiants avec les séminaires de recherche, à la fois en tant que spectateur et en temps que présentateur. Les élèves y seront encouragés à assister au séminaires des équipes de recherche du LaBRI et à discuter de leur expérience. Ils devront également préparer deux présentation, une première sur un problème ouvert, puis une seconde sur un article de recherche, qu’il retravailleront en fonction des retours. Ils devront également écouter leurs camarades faire leurs présentation et leur faire des critiques constructives, et poser des questions.

Voir la page complète

Objectifs : Lire un article scientifique.

Identifier les ressources connexes à la problématique scientifique ciblée par l'article (réaliser une étude bibliographique).

Rédiger un résumé des contributions apportées par l'article.

Présenter une synthèse de l'article.

Voir la page complète

Majeure en vérification logicielle, mineure en algorithmique avancée.

Voir la page complète

Voir la page complète

La théorie des graphes est un modèle très général qui permet de représenter des problèmatiques très variées, que ce soit dans les réseaux (de toute nature) mais aussi pour des structures hierarchisées comme les bases de données. La culture générale des problématiques de graphe que nous proposons dans ce cours ainsi que la connaissance des outils efficaces pour ces problématiques sont des atouts pour reconnaître et traiter les problèmes qu'elles modélisent.

Cet enseignement présente des notions avancées de théorie des graphes et familiarise l’étudiant avec certaines techniques de preuve classiques, liées notamment à la coloration de graphes. Quelques problèmes et conjectures classiques sont abordés.

Voir la page complète

Objectifs : introduire l’algorithmique distribuée; présenter les différents modèles et contraintes du calcul distribué ; présenter et analyser quelques algorithmiques classiques du domaine ; concevoir des algorithmes s'exécutant sur des systèmes distribués

Voir la page complète

Comprendre et mettre en oeuvre l'intérêt et les principes de la démarche de recherche fondamentale et/ou appliquée
Savoir se remettre en question, faire preuve d'esprit critique
Construire et développer une argumentation.


Connaître et mettre en application les principaux modèles mathématiques intervenant dans les différentes disciplines connexes du domaine Sciences et Technologies mais aussi des autres domaines
Maîtriser les bases de la logique et organiser un raisonnement mathématique.
être capable de traduire un problème simple en langage mathématique.
Connaître les principaux paradigmes de programmation et sélectionner un langage adapté à une situation donnée
Identifier les limites de l'informatique en termes de calculabilité et de complexité
Modéliser une situation concrète en un énoncé formel au moyen d'outils (e.g., automates, langages, grammaires, graphes)
Comprendre une preuve de correction d'algorithme (e.g., variants/invariants, induction, convergence)

Voir la page complète

Comprendre et mettre en oeuvre l'intérêt et les principes de la démarche de recherche fondamentale et/ou appliquée
Savoir se remettre en question, faire preuve d'esprit critique
Construire et développer une argumentation.


Connaître et mettre en application les principaux modèles mathématiques intervenant dans les différentes disciplines connexes du domaine Sciences et Technologies mais aussi des autres domaines
Maîtriser les bases de la logique et organiser un raisonnement mathématique.
Construire et rédiger une démonstration mathématique synthétique et rigoureuse.
être capable de traduire un problème simple en langage mathématique.
Connaître les principaux paradigmes de programmation et sélectionner un langage adapté à une situation donnée
Modéliser une situation concrète en un énoncé formel au moyen d'outils (e.g., automates, langages, grammaires, graphes)
Comprendre une preuve de correction d'algorithme (e.g., variants/invariants, induction, convergence)
Ecrire une preuve de correction d'algorithme

Voir la page complète

Voir la page complète

Ce cours introduit la logique des modèles finis, tels que les mots, les arbres et les graphes fini, ainsi que des logiques temporelles utilisées en vérification. Nous présenterons également les logiques de description qui servent à représenter de manière formelle des connaissances d’un domaine particulier (e.g. médecine) pour améliorer l’interrogation et le partage d'informations. On s’intéressera au pouvoir d’expression des logiques considérées, ainsi que des problèmes algorithmiques variés (validation de formule sur un modèle, satisfiabilité de formule, inférence logique, etc).

Nous aborderons également l’apprentissage d'automates et de formules LTL à partir d’exemples dans des contextes passifs et actifs. Nous discuterons des algorithmes associés à ces problèmes (bornes supérieures) ainsi que des questions de complexité (bornes inférieures). Si le temps le permet, nous mettrons également en lumière un lien étroit entre la théorie des automates et la complexité des circuits algébriques, et montrerons comment les résultats de l'une peuvent être appliqués à l'autre.

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

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

Le but de ce cours est de familiariser les étudiants avec les séminaires de recherche, à la fois en tant que spectateur et en temps que présentateur. Les élèves y seront encouragés à assister au séminaires des équipes de recherche du LaBRI et à discuter de leur expérience. Ils devront également préparer deux présentation, une première sur un problème ouvert, puis une seconde sur un article de recherche, qu’il retravailleront en fonction des retours. Ils devront également écouter leurs camarades faire leurs présentation et leur faire des critiques constructives, et poser des questions.

Voir la page complète

Objectifs : Lire un article scientifique.

Identifier les ressources connexes à la problématique scientifique ciblée par l'article (réaliser une étude bibliographique).

Rédiger un résumé des contributions apportées par l'article.

Présenter une synthèse de l'article.

Voir la page complète

Voir la page complète

Ce cours a pour but d'apprendre à utiliser la modélisation formelle comme outil de détection de bugs et de preuve de systèmes ou programmes informatiques.

Voir la page complète

Maîtriser les concepts fondamentaux de la spécification et de la preuve formelle de programme.
Acquérir des compétences pratiques dans ce domaine.

Voir la page complète