Cours suivis en première année
Concepts de démonstration, de correction et complétude d'un système de preuve. On étudie le calcul des propositions, la déduction naturelle, le λ-calcul, le calcul des prédicats, les séquents, les modèles de Kripke. On termine par un aperçu des logiques modale, épistémique, temporelle.
Décidabilité
On donne deux définitions du calcul, par machine de Turing et fonctions récursives de Kleene. On étudie les notions d'algorithme universel, ensembles récursifs, récursivement énumérables, récursivement inséparables. On montre deux théorèmes fondamentaux : smn et Rice. Problèmes indécidables, et enfin indécidabilité du calcul des prédicats.
Programmation
Introduction approfondie aux concepts et techniques de la programmation, essentiellement autour d'ocaml. On développe un double point de vue, d'une part la pratique de la programmation, et d'autre part la conception d'un langage de programmation. On aborde tous les aspects de Caml, du coeur à la programmation objet, en passant par les modules. On étudie bien sûr le système de types, le polymorphisme, l'inférence. Ouverture sur la preuve, la mobilité.
Algorithmique
On voit quelques paradigmes classiques : diviser pour régner, programmation dynamique, algorithmes gloutons, analyse amortie. On étudie la complexité de certains problèmes, comme le tri, le calcul matriciel. On aborde la NP-complétude, les réductions, des heuristiques.
Notion de système d'exploitation, complément sur les shells, construction d'applications sous Unix, systèmes de fichier, processus et communications interprocessus, compilation séparée et bibliothèques.
Architecture des ordinateurs
assuré par Jean Duprat
Histoire du calcul, représentation de l'information, circuits combinatoires, logique CMOS, l'ordinateur de Von Neumann, le processeur RISC, puis aperçu d'un système complet, et ouverture sur la synthèse VLSI, les systèmes asynchrones, et autres techniques avancées et exotiques.
Systèmes de réécriture, confluence, terminaison, unification, etc.
Graphes
assuré par Vincent Bouchitté
Ce cours est une initiation à la théorie des graphes et à la conception et l'étude des algorithmes de base du domaine. On aborde toutes les notions élémentaires : parcours, composantes connexes, tris, recherche du plus court chemin, flot maximum, coloration, etc.
Modélisation des systèmes complexes
assuré par Michel Morvan
Étude de systèmes dynamiques discrets, et lien avec la modélisation en sciences humaines ou biologie par exemple. Automates cellulaires, automates à seuil, tas de sable.
Systèmes d'exploitation
Cours sur les systèmes d'exploitations. En particulier sur Unix. En TD nous avons travaillé sur le système NACHOS.
Programmation Orientée Objet et Génie Logiciel. Projet réalisé en groupe de trois, ayant pour but de se former à la programmation orientée objet. L'accent est mis sur l'étape de modélisation (diagrammes UML).
Cours suivis en deuxième année
Sémantique
Sémantique opérationnelle : on associe à un programme la suite des états d'une machine (abstraite) qui l'exécute. Sémantique dénotationnelle : on associe à un programme la fonction mathématique qu'il calcule. Sémantique axiomatique : on associe à un programme l'ensemble des assertions logiques reliant ses sorties et ses entrées.
Automates Cellulaires (DEA)
Définition algorithmique, caractérisation mathématique. Différents types : surjectifs, injectifs, périodiques, nilpotents, additifs… Point de vue modèle de calcul (signaux, firing quad, puissance de calcul, reconnaissance de langages et classes de complexité). Point de vue systèmes dynamiques (différentes notions de chaos, le groupage comme moyen d'aborder la complexité).
Compilation
On a fait de l'analyse lexicale, de l'analyse syntaxique, de l'analyse sémantique (attributs et vérification de type). On a aussi étudié la génération de code, les optimisations globales et locales, l'allocation des registres, l'ordonnancement des instructions. On a aussi considéré le ramasse-miettes, la compilation des langages orientés objet et la compilation des langages parallèles.
Algorithmique parallèle
PRAM et complexité. Mémoire partagée, vectorisation, hiérarchie mémoire, algorithmes d'algèbre linéaire par blocs. Mémoire distribuée, réseaux d'interconnection, macro-communications, algorithmes d'algèbre linéaire. Ordonnancement, graphe de tâches et heuristiques classiques. Architectures spécialisées, introduction aux techniques de parallélisation automatique.
Conduite de projet logiciel
L'objectif était de donner aux étudiants une méthodologie leur permettant de mener à bien un projet logiciel de grande envergure.
Recherche opérationnelle
Algorithmes simples (optimisation à une dimension sans contraintes, ordonnancement, problèmes de flots, programmation dynamique). Programmation linéaire. Optimisation Combinatoire (programmation linéaire en nombres entiers, la méthode branch and bound). Heuristiques et méta-heuristiques (recuit simulé, tabou, algorithmes "génétiques"). Utilisation des méthodes de la RO en Informatique.
Mobilité
Méthodes pour la description et l'analyse des systèmes distribués et mobiles. Algèbres de processus pour la mobilité, notamment le π-calcul et les mobile ambients. Techniques pour raisonner sur ces modèles (systèmes de types, preuves de bisimulation, logiques).
Programmation fonctionnelle et preuves
λ-calcul pur avec types dépendants, Présentation imprédicative de la logique usuelle. Les types de données inductifs, démonstrations par récurrence et calcul récursif. Les propositions inductives, programmation logique et spécifications. Sortes et extraction de programmes. Récursion bien fondée. Programmation impérative. Démonstration par réflexion.
Projet de compilation
Réalisation d'un compilateur pour un sous-ensemble de PASCAL, vers de l'assembleur CRISC. Le compilateur a été écrit en OCaml.
Images
assuré par Bernard Peroche
On a vu des techniques permettant de générer des images de synthèse et d'interpréter des images réelles. Les différents concepts et méthodes associés à ces domaines ont étés présentés. On a aussi bénéficié d'une introduction pratique à OpenGL et au Ray-Tracing.
Systèmes Max-Plus
assuré par Bruno Gaujal
Algèbre Max-Plus, réseaux de Petri, graphes d'évènements, introduction aux probabilités, chaînes de Markov, chaînes de Markov en temps continu, processus de décision Markoviens.
Systèmes dynamiques discrets
assuré par Michel Morvan
Théorie du comportement de certains systèmes dynamiques classiques (déterministes et stochastiques). Comment de tels systèmes sont utilisés en pratique pour modéliser des situations issues de domaines scientifiques tels que les sciences humaines ou la biologie. Étude personnelle sur le thème des automates cellulaires hétérogènes (deux types de cellules).