M1 MPRI at ENS Paris-Saclay: Catalogue

WIRE: Initiation to Research Workshop

Description : Ce module a comme objectif de développer, par la pratique, les compétences spécifiques au travail de recherche. Ces compétences sont : évaluer l’état de l’art sur un problème ou domaine donné, formaliser un problème de recherche, présenter les résultats de recherche à des collègues, identifier les enjeux d’un domaine de recherche (importance,motivation, applications, perspectives), approprier les règles de la profession de chercheur. Les ateliers sont organisés en groupes de 6 à 8 étudiants sous la direction d’un enseignant-chercheur ou chercheur senior. Des tâches sont assignées à chaque participant toutes les semaines. Un travail personnel est nécessaire entre deux séances.

En savoir plus ...

ADCO: Advanced Complexity

Description : La théorie de la complexité va bien au-delà de celle de la NP-complétude. Le but de ce cours est d'aller regarder un certain nombre d'autres constructions fondamentales de la théorie de la complexité: complexité en espace, notions de machines alternantes, ou randomisées. On y verra quelques théorèmes fascinants: l'équivalence du temps alternant et de l'espace déterministe par exemple, ou le théorème IP=PSPACE de Shamir.

En savoir plus ...

AFIT: Algorithms for Formal Calculus and Information Theory

Description : Ce cours d'algorithmique avancée a comme but d'apprendre les algorithmes efficaces liés à l'algèbre effective et à la théorie d'information. Plus précisément, on étudiera les opérations sur les polynômes et les grands entiers, les codes correcteurs d'erreur et la compression de données.

En savoir plus ...

CBIO: Computational Bio-engineering

Description : La bio-ingénierie est une discipline en plein essor, avec des applications en bio-production, pharmacie, sciences de l'environnement et médecine. Elle repose sur des compétences issues de la biologie, de l'informatique, de la théorie du contrôle et d'autres domaines. À l'issue de ce cours, les étudiants seront capables de:

• Construire et utiliser des modèles mathématiques pour la bioingénierie.
• Appliquer des techniques de compilation, de contrôle et d'optimisation à un processus biologique.
• Analyser et exploiter des données expérimentales issues de la spectroscopie et de la microscopie.

En savoir plus ...

DONA: Distributed and Online Algorithms

Description : Ce cours d'algorithmique avancée a comme but d’acquérir des bases des probabilités appliquées aux algorithmes classiques et aux algorithmes en ligne, et les principes des algorithmes distribués. À l'issue de ce cours, les étudiants seront capables de: (1) Analyser des algorithmes randomisés en étudiant leur temps d'exécution espéré et leur probabilité d'erreur. (2) Expliquer et appliquer l'analyse compétitive aux algorithmes en ligne. (3) Comprendre les bases du raisonnement sur les algorithmes distribués et leurs contraintes.

En savoir plus ...

ICAT: Introduction to Categories

Description : La théorie des catégories s'intéresse notamment à l'étude des relations entre les structures présentes en mathématiques et dans les fondements de l'informatique. Des instances de concepts catégoriques abstraits apparaissent dans de nombreux domaines variés, auxquels des théorèmes catégoriques généraux peuvent ensuite être appliqués. Par exemple, le concept catégorique fondamental de « produit binaire » peut s'incarner dans la catégorie des ensembles (produit cartésien), dans celle des espaces vectoriels (somme directe) ou encore dans tout ensemble partiellement ordonné (borne inférieure). Des observations similaires s'appliquent, entre autres, aux concepts catégoriques de « foncteur », de « transformation naturelle » et de « monade ». La théorie des catégories fournit ainsi un niveau d'abstraction utile pour démontrer des résultats génériques. Par ailleurs, les catégories elles-mêmes peuvent servir de modèles pour des logiques et des théories des types. Cela établit un lien d'interaction étroit entre la théorie des catégories, la logique et les langages de programmation : la correspondance de Curry-Howard-Lambek. À titre d'exemple, la notion catégorique de « monade » a été transposée aux langages de programmation fonctionnelle tels que Haskell. Les méthodes catégoriques jouent également un rôle majeur dans la recherche sur la sémantique des langages à types dépendants (comme Agda, Lean et Rocq) et sont utilisées dans le domaine de l'informatique quantique. Enfin, au cours de cet enseignement, nous pourrons également évoquer certains liens entre la théorie des catégories et la théorie des automates.

En savoir plus ...

IVER: Introduction to Verification

Description: Le cours donne une introduction aux techniques de model-checking, utilisés pour vérifier la fiabilité des systèmes critiques. On commencera par la modélisation des systèmes à événements discrets, des systèmes de transition enrichis avec des structures de données pour communiquer (variables, messages) et avec de différents méthodes de synchronisation. Ensuite, on étudie les logiques temporelles (linéaires et branchues) pour exprimer des propriétés à vérifier, notamment LTL, CTL et CTL*. Nous étudions leur expressivité, leur décidabilité et la complexité de certains problèmes associés.

La deuxième partie du cours est consacré aux méthodes avancées pour pallier le problème d'explosion d'états. Notamment, on étudie les diagrammes de décision binaires (BDD), les réductions à ordre partiel et le cycle d'abstraction-raffinement guidé par des contre-exemples, ainsi que les notions de similarité et bisimilarité. La plupart du cours s'occupe de la vérification des systèmes à état fini. Comme introduction au model-checking des systèmes infinis, on étudie les réseaux de Petri et les automates à pile.

En savoir plus ...

LAIK: Logic for AI: Knowledge Logics

Description : Ce cours s'intéresse aux aspects logiques de l'intelligence artificielle dans l'objectif de raisonner formellement sur la connaissance d'agents ou de coalitions d'agents. Les méthodes présentées dans ce cours sont issues des fondements en logique et en théorie des automates, ainsi que de l'approche model-checking pour la vérification de programmes. Plusieurs familles de formalismes logiques sont introduites dans ce cours, incluant les logiques de description (dont ALC, les logiques temporelles stratégiques (dont ATL), ainsi que des formalismes similaires.

En savoir plus ...

PACS: Probabilistic Aspects of Computer Science

Description: L'objectif de ce cours est d'introduire les principaux modèles de systèmes à événements discrets (chaînes de Markov, processus de décision markovien, automates probabilistes), leur théorie et les algorithmes associés. D'autre part, de présenter la théorie des graphes aléatoires un formalisme particulièrement adapté à la modélisation de systèmes distribués large échelle tels que les réseaux de télécommunication ou les réseaux sociaux. Ce cours vous prépare aux cours de la thématique Automata/Games du M2 MPRI.

En savoir plus ...

PROT: Proof Theory

Description : Dans une preuve mathématique, on peut distinguer des étapes de raisonnement et des étapes de calcul. Ce cours a pour objectif de fournir un cadre général dans lequel exprimer ces deux aspects, et d'acquérir les outils de base permettant de s'assurer des bonnes propriétés des règles de calcul utilisées (terminaison, confluence, modèles). Il fournit également une introduction aux types dépendants et comment ceux-ci peuvent être utilisés pour représenter les formules et les preuves de différentes logiques de manière modulaire.

En savoir plus ...

TAIG: Tools for AI: Game theory

Description : Ce cours propose une introduction aux concepts fondamentaux de la théorie des jeux, destinée aux étudiants en informatique. L'accent est mis sur les principaux modèles et concepts de solution, ainsi que sur leurs aspects algorithmiques. Le cours aborde les jeux stratégiques, les jeux sous forme extensive et les jeux sur graphes.

Les liens avec l'intelligence artificielle sont illustrés notamment par la recherche adversariale, l'apprentissage dans les jeux, la résolution de jeux et l'apprentissage par renforcement. Le cours fournit également les bases de théorie des jeux utiles pour suivre ensuite le cours de Mechanism Design.

En savoir plus ...

TAIS: Tools for AI: Solvers

Description : Ce cours introduit les principaux outils du raisonnement automatique, un domaine dont l'objectif est d'apprendre et de produire des nouvelles connaissances automatiquement, à partir d'une représentation logique des systèmes. Le cours aborde les algorithmes pour décider le problème de la satisfiabilité d'une formule dans différents fragments de la logique du premier ordre (logique propositionnelle, contraintes d'égalité entre termes, arithmétique linéaire sur les réels et entiers) utilisés dans les domaines de la vérification et la synthèse de programmes. La combinaison des ces algorithmes par le principe de Nelson-Oppen ainsi que la programmation par contraintes sont également étudiées. Les connaissances théoriques seront appliquées à la résolution de problèmes en utilisant les outils existants (CVC, Z3) et au codage de nouvelles procédures de décision.

En savoir plus ...

ACOM: Advanced Compilation

Description : Ce cours est une introduction à la compilation. On y explique les techniques et outils utilisés dans les différentes phases d'un compilateur, jusqu'à la production de code assembleur optimisé.

En savoir plus ...

APSA: APproximation and String Algorithms

Description : Ce cours d'algorithmique avancée a pour objectif d'initier les étudiants aux fondements des algorithmes appliqués aux chaînes de caractères, aux algorithmes d'approximation, et à la programmation linéaire. Les concepts étudiés incluent la conception d'algorithmes efficaces pour des problèmes classiques, pour des problèmes d'approximation, ainsi que les applications des techniques de programmation linéaire.

En savoir plus ...

ADSE: ADvanced Software Engineering

Description : Le cours introduit les méthodologies utiles pour le développement des applications logiciel et qui sont indépendantes du langage de programmation choisi. Ces méthodes permettent de capturer les besoins des utilisateurs, de concevoir l'application à un niveau indépendant du langage de programmation, d'organiser le travail de groupe, de prévenir, détecter et corriger les erreurs, de faciliter la maintenance du code et d'obtenir un produit logiciel robuste. Les leçons donneront les bases de la modélisation, de la conception et du développement rigoureux du logiciel, ainsi que les les méthodes de test et la gestion des versions. Les étudiants appliqueront ces méthodologies dans un projet par groupe de 3 à 6. Dans une première étape, les étudiants choisiront un sujet parmi ceux proposés, complèteront le cahier de charge et proposeront une conception détaillée de l'application. Dans une seconde étape (deuxième période), ils développeront le projet et le valideront en utilisant les techniques apprises. L'évaluation du projet prendra en compte tous les aspects du projet: la conception, le codage, la validation, la coordination du travail, la documentation et le logiciel délivré.

En savoir plus ...

NETS: Networks

Description : Ce module présente les concepts principaux utilisés dans les réseaux informatiques, tels que l'adressage, l'échange de données, le routage et les protocoles de transport. L'approche adoptée est formelle, en illustrant ces concepts à l'aide de modèles comme les diagrammes de séquences de messages et les automates communicants. Le module introduit également la programmation de sockets et propose comme projet la programmation d'une application distribuée.

En savoir plus ...

ISEC: Security

Description : Ce module est une introduction à la modélisation et à la preuve de protocoles cryptographiques. Pour la partie modélisation, on présentera une algèbre de processus permettant de modéliser des ensembles d'agents communicants et à un langage pour exprimer les propriétés de sécurités attendues d'un protocole cryptographique telles que l'authentification, le secret de certaines données ou l'anonymat. On étudiera également une abstractions symboliques de la cryptographie (i.e. le modèle Dolev-Yao) et des procédures de décision et semi décision de la sécurité pour certaines classes de protocoles. Le cours proposera également une brève ouverture sur des techniques de preuves à base de réductions dans le cas où on n'abstrait pas la cryptographie (i.e. dans le modèle calculatoire).

En savoir plus ...

OMD: Mechanism design

Description : Ce cours porte sur la conception de mécanismes visant à régir les interactions entre individus stratégiques afin d'obtenir des résultats souhaitables. Un thème central sera l'arbitrage entre l'optimalité d'un objectif — tel que les recettes ou le bien-être social — et d'autres propriétés désirables comme la simplicité, la robustesse, la faisabilité computationnelle et la praticité. Cet arbitrage sera quantifié à l'aide d'une théorie de l'approximation mesurant la perte de performance d'un mécanisme d'approximation simple, robuste et pratique par rapport au mécanisme optimal, souvent complexe et délicat. Le cours met l'accent sur les techniques permettant de mener cette analyse, ainsi que sur les conclusions économiques et les implications pratiques qui en découlent.

En savoir plus ...