L'objectif est l'acquisition des outils théoriques permettant de construire un raisonnement, avec application à la preuve de programmes.
- Logique propositionnelle
- Logique des prédicats
- Induction
- Preuve formelle
- Spécification et sémantique des programmes
- Preuve de terminaison de programmes
- Preuve de correction de programmes
L'objectif de ce cours est de présenter comment fonctionnent les principaux éléments architecturaux d'un ordinateur. Le plan du cours est le suivant:
- Codage de l'information, des entiers, flottants jusqu'aux instructions et programmes
- Fonctionnement des unités fonctionnelles d'un processeur
- Améliorations architecturales: pipeline, VLIW, superscalaire et out of order, unités vectorielles
- Fonctionnement de la hiérarchie mémoire: mémoire principale, fonctionnement des caches, prefetch, mécanisme de pagination.
- Programmation des d'entrées sorties, DMA, bus
- Structure de multicoeur, hiérarchie mémoire pour multicoeurs.
L'objectif de ce cours est d'apprendre les bases de la
programmation impérative par l'étude de la syntaxe et la sémantique du
langage C.