Peter Habermehl - Enseignement "Logique et Vérification"

Module "Logique et Vérification"
IUP 3

Présentation

Pré-requis : logique booléenne.
Objectif : Présenter les concepts et les méthodes de base de la logique et ses applications pour la vérification de programmes.
Plan du cours :
- Notions de base de logique :
  - Logique propositionnelle
  - Diagrammes de décision binaire (BDD)
- Logiques temporelles et vérification de systèmes concurrents
  - Logique linéaire et arborescente
  - Modélisation de systèmes concurrents en utilisant les automates communiquants
  - Evaluation d'une formule sur un modèle (model-checking)
  - Model-checking symbolique
  - Logique et automates temporisés
Bibliographie :
- Ph. Schnoebelen, B. Bérard, M. Bidoit, F. Laroussinie, A. Petit. Vérification de logiciels : Techniques et outils du model-checking. Vuibert, 1999
- E.M. Clarke, O. Grumberg, D. Peled. Model Checking. MIT Press 2000.
- Cours sur les BDDs

Organisation

Cours : Le responsable du cours est Peter Habermehl (adresse e-mail Peter.Habermehl(at)liafa.jussieu.fr, bureau 6A13). L'enseignement a lieu le premier semestre. Le premier cours a lieu le 1 octobre. L'horaire du cours est le suivant :

Jour Heure Salle

Jeudi 8h30 J8

TD et TP : Le responsable des TD/TP est Antoine Meyer En général, les sujets des TD/TP suivent à peu près le cours de la semaine précédante. Le premier TD a lieu la semaine du 6 octobre. L'horaire des TD/TP est le suivant :

Travaux Jour Heure Salle

dirigés Mercredi 16h30 J7

pratiques Mercredi 14h30 TP 108

Evaluation : La note finale est calculée comme (2*Ex + CC)/3 où Ex est la note de l'examen et CC est la note du contrôle continu. En Septembre, la note est la note d'examen.
- Examen : Date à fixer en janvier.

Jour	Heure	Salle
Jeudi	8h30	J8

Travaux	Jour	Heure	Salle
dirigés	Mercredi	16h30	J7
pratiques	Mercredi	14h30	TP 108

Calendrier et polycopies

Semaine du	Cours	TD	TP	Observations
29 sep.	CM-1 (logique propositionnelle, resolution) Transparents	-	-	-
6 oct.	CM-2 (BDDs) Transparents	TD/TP 1	-	-
13 oct.	CM-3 (Modélisation) Transparents	TD/TP 2	-	-
20 oct.	CM-4 (Suite Modélisation)	TD 3	TP 3	-
27 oct.	CM-5 (Logique temporelle linéaire) Transparents	TD 4	-	-
3 nov.	CM-6 (Logique temporelle arborescente) Transparents	-	TP 4	-
10 nov.	CM-7 (Logique temporelle arborescente)	-	TP 5	-
17 nov.	CM-8 (Logique temporelle arborescente)	-	-	-
24 nov.	CM-9 (Logique temporelle arborescente) Transparents	-	-	Partiel pendant le TP
1 dec.	CM-10 (Contraintes d'équité) Transparents	-	-	-
8 dec.	-	-	-	-

Liens

Les liens WEB suivants peuvent vous être utiles :