INFO 0009-1 Bases
de données (organisation générale)
Introduction aux bases de données et à la
modélisation des informations. Modèle entité-rélation.
Bases de données relationnelles et langages d'interrogation.
Théorie des dépendances et conception des schémas
de bases de données relationnelles. Organisation physique des
données et implémentation du modèle
relationnel. Gestion des transactions. Bases de données
déductives, orientées-objet, hiérarchiques et
en réseau.
INF0 0012-1 Structure
des ordinateurs
Etude détaillée d'un
processeur et d'un langage d'assemblage. Bases de la programmation
système et de la gestion de processus; mémoire
virtuelle. Programmation parallèle et principaux
mécanismes de communication entre processus. Techniques
d'implémentation des processeurs: pipe-line, mémoire
cache, ... Travaux pratiques: Séances d'exercices,
travaux portant principalement sur la programmation parallèle.
INFO 0016-1 Introduction
à la calculabilité
Introduction à la
notion de procédure effective. Ensembles énumérables
et non énumérables. Automates finis et à pile.
Grammaires formelles et leur relation à la théorie des
automates. Machines de Turing et thèse de Turing-Church.
Théorie des fonctions récursives. Problèmes
insolubles par une procédure effective. Introduction à
la NP complétude et à la théorie de la
complexité.
INFO 0039-2 Projet
de programmation orientée-objet
Réalisation
d'un projet de programmation substantiel par équipes. Le
langage de programmation utilisé est le JAVA.
INFO 0060-1 Vérification
de systèmes parallèles et logique temporelle (en
collaboration avec P.
Gribomont )
Le cours comporte deux parties. La première
est consacrée à la vérification algorithmique
de systèmes parallèles basée sur l'exploration
de l'espace des états. Elle couvre les techniques
d'exploration de l'espace des états, les optimisations
possibles de cette exploration et son utilisation pour la
vérification de formules de logique temporelle par
``vérification de modèle'' (model checking). Ce
dernier problème est traité à l'aide des
automates sur mots infinis auxquels une introduction est donnée.
La deuxième partie introduit la méthode des
invariants et des assertions inductives. On étudie des
techniques permettant de construire des invariants et des techniques
permettant de les valider. On s'intéresse spécialement
aux outils permettant d'automatiser en partie le processus de
vérification, et au cas particulier fréquent où
la majorité des variables du système à vérifier
sont booléennes.
Sujets
de travaux de fin d'études (année académique
2008-2009)