Informations sur les cours de P. Wolper

• INFO 0009-1 & INFO 0009-2 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-2 &  INF0 0012-3 Computation Structures
  Detailed study of a processor and of an assembly language. Introduction to systems programmning and to processes; virtual memory. Concurrent programming and interprocess communication. Processor implementaton techniques: pipe-lines, cache memory, ... 

• INFO 0016-1 Introduction to the theory of computation
  Introduction to the concept of effective procedure. Countable and uncountable sets. Finite automata and pushdown automata. Formal grammars and their relation to automata. Turing machines and the Church-Turing thesis. Theory of recursive functions. Problems unsolvable by an effective procedure. Introduction to NP-completeness and complexity theory.
   
• INFO 0060-1 Vérification de systèmes parallèles et logique temporelle (en collaboration avec  B. Boigelot et   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.