Mihaela Sighireanu - Enseignement "Logique et vérification"

Module "Logique et vérification"

IUP 3ème année

Année 2001-2002

Présentation (prérequis, objectif, contenu, bibliographie)
Organisation (cours, TD, TP, évaluation)
Calendrier et polycopies (cours, TD, TP)
Liens (pages web pour les outils)
Archives

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 :
- I. Guessarian et A. Arnold. Mathématique pour l'informatique, Eyrolles, 1994
- E. Audureau, P. Enjalbert, L. Fariñas del Cerro. Logique temporelle : sémantique et validation de programmes parallèles. Masson, 1990
- Z. Manna, A. Pnueli. Temporal Verification of Reactive Systems. Springer-Verlag, 1995
- 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.

Organisation

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

Jour Heure Salle

Jeudi 10h30 J5

TD et TP : Le responsable des TD/TP est Mihaela Sighireanu (adresse e-mail Mihaela.Sighireanu@liafa.jussieu.fr, bureau 6A27). 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 15 octobre. Les logiciels utilisés en TP sont installés sur la machine cunillet. L'horaire des TD/TP est le suivant :

Travaux Jour Heure Salle

dirigés Mardi 9h00 J5

pratiques Lundi 16h30 TP 2 sur cunillet

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.
- Examen : Date à fixer en janvier.
- Contrôle continu : Le travail fait pendant les heures de TP sera évalué par un devoir dont le sujet se trouve ici. En résumé, il s'agit principalement de la modélisation et de la vérification d'algorithmes distribués ou des protocoles.
  Au plus tard le 18 décembre 2001 (l'heure de réception faisant foi), vous devez renvoyer le code de vos devoirs et les rapports décrivant votre code, par courrier électronique à l'adresse suivante : Mihaela.Sighireanu@liafa.jussieu.fr. Un e-mail d'acquittement vous sera envoyé dans les 24h de votre envoi (sauf le weekend). Uniquement après la réception de cet acquittement vous pouvez considérer que votre devoir a été reçu.
- Précisions importantes :
  Les devoirs du contrôle continu doivent être rendus à la date précisée. Les soumissions en retard seront acceptés (selon la volonté des enseignants) avec 10% de pénalité par jour. Aucune soumission ne sera acceptée après la date de l'examen.
  Toute problème d'e-mail (adresse incorrecte, panne du serveur, coupure d'électricité, etc.) n'est pas considérée comme une excuse valide. C'est pourquoi nous vous recommandons de ne pas envoyer votre devoir à la dernière minute.
  Vous devez travailler seuls sur tous les devoirs. Vous êtes encouragés à consulter vos collègues sur la manière de résoudre ces devoirs. Toutefois, tout travail et soumission doit être faite individuellement.
  Toute copie d'un devoir sur un collègue sera sanctionnée comme une copie à l'examen.

Jour	Heure	Salle
Jeudi	10h30	J5

Travaux	Jour	Heure	Salle
dirigés	Mardi	9h00	J5
pratiques	Lundi	16h30	TP 2 sur cunillet

Calendrier et polycopies

Semaine du	Cours	TD	TP	Observations
8 oct.	CM-1 (resolution, logique propositionnelle)	-	-	-
15 oct.	CM-2 (BDD)	TD-1 [html, ps] (logique propositionnelle)	-	-
22 oct.	CM-3 (BDD et automates)	TD-2 [html, ps] (BDD)	TP-1 [html, ps] (GUI BDD)	-
29 oct.	-	TD-3 (BDD, resolution)	TP-2 (CMU BDD)	pas de cours-ferie
5 nov.	CM-4 (BDD et automates)	-	-	-
12 nov.	CM-5 (LTL)	TD-4 [html, ps] (Modélisation de protocoles)	TP-4 (Spin)	-
19 nov.	CM-6 (CTL)	TD-5 (LTL)	TP-5 (Spin)	-
26 nov.	CM-7 (MSC)	TD-6 (CTL)	TP-6 (SMV)	-
3 dec.	CM-8 (Systèmes temporisés, TCTL)	TD-7 (CTL)	TP-7 (SMV)	-
10 dec.	CM-9 (TCTL)	TD-8 (TCTL)	TP-8 (Uppaal)	-
17 dec.	CM-10 (Systèmes temporisés)	TD-9 (Systèmes temporisés, TCTL)	TP-9 (Uppaal)	-

Liens

Les liens WEB suivants peuvent vous être utiles :

Archives

Année 1999-2000

Année 2000-2001

Pour toute information sur les cours, TD et TP contactez les enseignants.

Dernière modification : Fri Oct 5 14:36:06 2001
URL: http://www.liafa.jussieu.fr/~sighirea/cours/logver/index.html