-
Avec des interventions par Hubert Comon-Lundh (a priori le 21 déc.),
Stéphane Demri, et Claude Kirchner.
Le cours a lieu de 16h00 à 19h00.
Le poly pour ma partie; on ne fera pas tout dedans, rassurez-vous!
Mais le théorème 8 (complétude) sera un gros morceau, et important.
Voir les pages Web des autres intervenants pour les polys correspondant à leurs parties.
- Devoir à la maison à rendre pour le 16 novembre 2004. La
première version a été distribuée à la séance du 12 octobre 2004.
Nouvelle nouvelle3 version corrigée en date du 08 novembre 2004, faisant suite à celles du 05 novembre 2004 et du 20 octobre 2004.
20 oct. 2004: Il y avait une erreur dans l'énoncé de la question I.1 (lire "sinon I_{k+1} = I_k U {-/+ A_k^0}" au lieu de "sinon I_{k+1} = I_k"). De plus, l'énoncé de la question II.3 était imprécis.
04 nov. 2004: l'énoncé de la question I.3 était tout simplement faux.
La question I.3 est censée être une application directe des questions précédentes.
05 nov. 2004: en question II.1, le dernier cas de la fonction de sélection contenait une erreur d'exposant (un + au lieu d'un -).
08 nov. 2004: en question II.1, il n'était pas clair que la simulation devait utiliser les clauses de Def aussi. On pouvait l'inférer à partir de la question II.2.
La fin des cours fondamentaux est le 07 décembre. A partir du 14 décembre commencent les cours optionnels. A priori (ça peut bouger):
- 14 décembre. Jean-Pierre Jouannaud, réécritures quotients, réécriture d'ordre supérieur et applications;
- 04 janvier. Hubert Comon-Lundh, Théories locales, déductions en temps polynomial et applications;
- 11 janvier. Jean Goubault-Larrecq, Classes décidables par résolution, automates bidirectionnels et applications;
- 18 janvier. Claude Marché, Combinaisons de théories, algorithme de Shostak;
- 25 janvier. Stéphane Demri, Logiques modales et tableaux;
- 01 février. Claude Kirchner, Déduction modulo et applications;
- 15 février. Examen.
-
|
Cours |
TD |
|
Où?
à l'ENS Cachan, bâtiment Cournot
|
Salle 307
|
|
Quand?
|
à partir du vendredi 03 octobre 2003
|
|
Par qui?
|
Jean Goubault-Larrecq
|
Première séance: vendredi 03 octobre 2003, 9h00-13h00.
Le cours a lieu en salle Cournot 404.
Le but de ce cours est de comprendre comment les langages de
programmation s'articulent autour de la notion de sémantique,
et d'illustrer ceci au travers de la réalisation en projet d'un
mini-compilateur pour un langage-jouet, vers le langage machine.
Le programme du cours 2002 avec les copies des transparents, était ici. Mais en 2003, tout change! Voir la table des matières, en ps ou en pdf.
- 1. Vendredi 03 octobre 2003, 9h00-13h00. Introduction aux langages de
programmation; treillis, cpos, points fixes.
ps, pdf.
- 2. Vendredi 10 octobre 2003, 9h30-13h00. Structures de données de base, affectations, procédures; langages fonctionnels.
ps, pdf.
- 3. Vendredi 17 octobre 2003, 9h30-13h00. Un peu plus loin dans le cambouis: l'assembleur; toujours plus loin dans la théorie: sémantique dénotationnelle de mini-Caml, modèle de Plotkin.
ps, pdf.
- 4. Vendredi 24 octobre 2003, 9h00-10h55. Sémantique dénotationnelle, de mini-Caml en particulier.
ps, pdf.
Je vous propose d'occuper les deux heures que vous aurez de libre
entre 11h00 et 13h00 à commencer le devoir à la maison que je vous donnerai à faire à 10h55...
- 5. Vendredi 07 novembre 2003, 9h00-13h00. Cours d'architecture des ordinateurs, partie 1, par Béatrice Bérard.
- 6. Vendredi 14 novembre 2003, 9h00-13h00. Cours d'architecture des ordinateurs, partie 2, par Béatrice Bérard.
- 7. Vendredi 21 novembre 2003, 9h30-13h00.
Sémantique opérationnelle de mini-Caml. Sémantiques concrètes et abstraites, clôtures. Modes d'appel: par valeur/par nécessité, par valeur/par référence, gauche-droite/droite-gauche/ordre non déterminé. Liaison lexicale/portée dynaminque. Dérivations, récurrence structurelle sur les dérivations. Déterminisme. Règles dérivées. Théorème de correction.
ps, pdf.
- 8. Vendredi 28 novembre 2003, 9h30-13h00.
Dernier cours de programmation, on termine la leçon 5, et on finit en beauté
en parlant de correction et de points fixes: 9h30-11h00.
De 11h00 à 13h00, premier cours par Delia Kesner.
Une annexe contenant un guide rapide de l'assembleur Pentium
est disponible en ps ou en pdf.
Le poly en un seul bloc en ps ou en pdf.
Le corrigé de certains exercices du poly, donnés en devoir à la maison:
ps ou pdf.
Le partiel (à la maison): sujet en ps ou en pdf. Corrigé: ps ou en pdf.
Suite du cours avec Delia
Kesner. Attention: à partir du vendredi 05 décembre 2003, 9h00-13h00, même salle.
-
Cours de la filière "preuves" du DEA
Programmation.
|
Cours |
|
Où?
à Paris VII, 175-179 rue du Chevaleret Paris 13ème
(métro Chevaleret)
|
Salle 6C1 (anc. 0D4)
|
|
Quand?
|
le mercredi après-midi, 14h-16h,
à partir du 7 janvier 2004
|
|
Par qui?
|
Hubert Comon-Lundh
|
|
Jean Goubault-Larrecq
|
Programme :
- 11 février: automates d'arbres, clauses de Horn, codage
des protocoles cryptographiques en clauses de Horn, à la Blanchet;
- 18 février: relâche;
- 25 février: démonstration automatique,
indécidabilité,
résolution, complétude par arbres sémantiques, stratégies ordonnées,
subsomption (JGL);
- 03 mars: décision de la classe H1 par résolution ordonnée
avec sélection, extraction d'un modèle (automate alternant)
d'un ensemble saturé de clauses;
- 10 mars: classes décidables de la logique du premier ordre, contraintes ensemblistes;
- 17 mars: model-checking de clauses par rapport à des modèles décrits par automates d'arbres alternants, extraction de preuve Coq, et certification de protocoles cryptographiques.
- 24 mars: examen. Voici le sujet, à préparer chez vous, soigneusement; vous en aurez besoin pour répondre aux 4 questions supplémentaires qui vous serons posées le 24 mars; sans compter les questions d'Hubert, bien sûr.
Note (le 22 mars 2004, 16h30): je viens de changer légèrement le sujet. En question 5, je demande k supérieur ou égal à 1, il s'agit d'un point technique de détail. Plus sérieusement, vous avez sans doute eu des difficultés avec la question 6. Elle était infaisable. Son énoncé a complètement changé. Elle reste cependant de loin la question la plus difficile de toute l'épreuve. Soyez rassuré, les questions supplémentaires de l'épreuve du 24 seront plutôt du niveau des questions 1 à 4...
Note (le 23 mars 2004, 14h00): j'ai encore légèrement modifié l'énoncé, et rappelé dans l'énoncé la définition de la classe H1, donnée en cours mais uniquement à l'oral. (Elle est aussi dans l'examen de l'année dernière, mais relativement difficile à extraire.)
Sujet complet: le voici, il y avait quatre questions supplémentaires (8-11), assez faciles. Voici aussi le corrigé.
Références :
- [GL02]
- Jean Goubault-Larrecq.
Vérification de protocoles cryptographiques : la logique à la rescousse !.
In J. Goubault-Larrecq, editor, Actes du 1er workshop international sur
la sécurité des communications sur Internet (SECI'02), Tunis,
Tunisia, Sep. 2002, pages 119-152. INRIA, 2002.
- [GL03]
- Jean Goubault-Larrecq.
Résolution ordonnée avec sélection et classes décidables de la logique du premier ordre. Notes de cours. Attention, nouvelle version du 06 octobre 2004 du poly.
- [GL04]
- Jean Goubault-Larrecq.
Une fois qu'on n'a pas trouvé de preuve, comment le faire comprendre à
un assistant de preuve?.
In V. Ménissier-Morain, editor, Actes des 15èmes journées francophones des
langages applicatifs (JFLA'04), Ste-Marie-de-Ré, France, janvier 2004,
pages 1-20. INRIA, 2004.
- [CLC02]
- Hubert Comon-Lundh et Véronique Cortier.
Security properties: Two agents are sufficient.
Research Report LSV-02-10, Lab. Specification and Verification, ENS de Cachan,
Cachan, France, August 2002.
26 pages.
- [C02]
- Véronique Cortier.
Observational equivalence and trace equivalence in an extension of
Spi-calculus. Application to cryptographic protocols analysis. Extended
version.
Research Report LSV-02-3, Lab. Specification and Verification, ENS de Cachan,
Cachan, France, March 2002.
33 pages.
- [TATA02]
- Hubert Comon et Max Dauchet et Rémi Gilleron et Denis Lugiez
et Sophie Tison et Marc Tommasi.
Tree Automata Techniques and Applications.
- [DLMS99]
- Nancy A. Durgin, Patrick Lincoln, John Mitchell, et Andre Scedrov.
Undecidability of bounded security protocols. Workshop on Formal Methods and Security Protocols (FMSP'99), Trento, Italy, July 5, 1999.
- [McA93]
- David A. McAllester.
Automatic recognition of tractability in inference relations. Journal of the ACM, vol.40, no.2, avril 1993.
Examens des années précédentes :
- (2003) La classe H1 de Nielson, Nielson et Seidl. L'examen se
déroulait en deux parties, la première partie était à faire à la
maison, et consistait en deux sujets, un sur la déduction par un intrus de Dolev-Yao en
présence de chiffrement par blocs, l'autre sur la décision de la non-vacuité d'une variante
d'automates d'arbres. Les étudiants devaient faire les
deux sujets, et étaient disponibles depuis le jeudi
20 mars 2003 à 10h00.
La deuxième partie s'est déroulée le mercredi 26 mars 2003 en salle 6C1
à Chevaleret. Elle consistait en une série de questions complémentaires
aux deux sujets, voici par exemple la seconde partie
complète.
Corrigé de la deuxième partie.
Pour plus de détails, voir l'article original.
-
(Cours commun au magistère MMFAI de l'ENS rue d'Ulm et au magistère Math-Info de l'ENS Cachan.)
|
Cours |
TD |
|
Où?
à l'ENS, 45 rue d'Ulm Paris 5ème
(RER Luxembourg)
|
Salle R, niveau -2 |
Salle U ou V, niveau -2 |
|
Quand?
|
le mercredi de 9h30 à 11h30
|
le mardi de 13h30 à 15h30
|
|
à partir du 18 février 2004 |
à partir du 24 février 2004 |
|
Par qui?
|
Jean Goubault-Larrecq
|
Florent Jacquemard
|
Notes de cours :
- Introduction : ps html;
- Lambda-calcul pur : ps html;
- Logique et types : ps html;
- Machines (en cours de rédaction) : ps html.
Examens des années précédentes :
- (2000) Relations logiques et théorème de Friedman, énoncé et correction;
- (2001) Lambda-upsilon calcul, types intersection et préservation de la normalisation forte, énoncé et correction.
- (2002) Le lambda-calcul monadique (ou méta-langage de Moggi), énoncé et correction.
- (2003) Lambda-upsilon calcul (le retour!), confluence et machines, énoncé; correction.
- (2004) Réductions closes, énoncé; correction.
- (2005) Systèmes de types intersection et modèles de filtres, énoncé; correction.
-
Désolé, pas encore d'info sur ces cours. Les deux cours ont eu lieu
en 2004-2005 à l'ENS Cachan. Ils font suite aux cours donnés les années
précédentes par Ralf
Treinen.
Le cours est basé essentiellement sur les notes de cours de Ralf,
et le Papadimitriou.
Programme abrégé:
- Complexité I: classes en temps, en espace; théorèmes de speedup, théorème du gap de Borodin, réductions en espace logarithmique, théorème de Cook (SAT est NP-complet), théorème de Savitch
(NSPACE(f(n)) inclus dans SPACE(f(n) carré)). Le cours de complexité I est
la suite du cours de calculabilité d'Hubert Comon-Lundh.
- Complexité II: théorème d'Immerman-Szelépcsenyi (les langages non déterministes en espace sont clos par complémentaires), théorème de Fagin et variantes
(NP est la classe des problèmes de graphes définissables en logique existentielle du second ordre), la hiérarchie polynomiale, PSPACE, QBF et le théorème de Wrathall (QBF est PSPACE-complet), machines alternantes (ALOGSPACE=P, APTIME=PSPACE), classes randomisées (RP, ZPP, BPP et leurs petits amis), le théorème de Shamir (IP=PSPACE).
Examens des années précédentes (complexité I) :
- (2005) Complexité du coloriage de graphes, énoncé; correction.
Examens des années précédentes (complexité II) :
- (2005) Problèmes de non-vacuité d'automates, énoncé; correction.
-
|
Cours |
TD |
|
Où?
au CNAM 292, rue Saint-Martin, Paris 3ème
(métro Réaumur-Sébastopol)
|
Salle 31 3 11 |
Salle 31 3 11 (ou autre pour les TP sur machine) |
|
Quand?
|
le mardi de 13h à 15h
|
le mardi de 15h à 17h
|
|
à partir du 08 janvier 2002 |
à partir du 08 janvier 2002 |
|
Par qui?
|
Jean Goubault-Larrecq
|
Fabrice Parrennes
|
Avertissement : les notes contiennent quelques petites erreurs,
je les ai laissées pour voir si vous suiviez...
Un petit texte d'introduction, à
paraître dans un ouvrage collectif publié chez
Hermès.
Notes de cours... sous forme de transparents :
- Cours 1 : Introduction, applications,
idées de base (règle des signes), sémantique
concrète;
- Cours 2 : une première
tentative d'écriture d'un analyseur abstrait pour la
règle des signes, notions d'approximation,
concrétisations;
- Cours 3 : abstractions, notion de
meilleure approximation, correspondances de Galois, application
à la sûreté du typage;
- Cours 4 : interprétation
abstraite de programmes, graphes de contrôle, sémantique
opérationnelle à petits pas, traces, sémantique
collectrice;
- Cours 5 : sémantique abstraite,
théorèmes de Knaster-Tarski, de Cousot, construction
formelle de l'interprétation abstraite, réalisation en
Caml, terminaison de l'analyse;
- Cours 6 : applications à la
détection de variables non initialisées, comment mélanger
plusieurs analyses, produit réduit;
- Cours 7 : applications aux débordements
arithmétiques, aux débordements de tableaux, treillis
des intervalles, élargissements;
- Cours 8 : analyses arrière,
debugging abstrait, slicing, itérations décroissantes locales,
combinaisons d'analyses avant et arrière;
- Cours 9 : tout le reste...
Examens des années précédentes :
- (2000) énoncé et correction;
- (2001) énoncé et correction.
Le projet!
-
Quelques exposés
- L'exposé "Pirates et sécurité informatique : la logique à la rescousse !" du 28 septembre 2001 et du 07 décembre 2001 : ps pdf;
- L'exposé "Cryptographie et protocoles cryptographiques" du 29 avril 2003,
au département économie et gestion : ps pdf;
- L'exposé "Relations logiques pour types monadiques ... et homologie?" du séminaire CATIA, Université Montpellier II, 14 février 2003 : ps pdf;
- L'exposé "Une fois qu'on n'a pas trouvé de preuve,
comment le faire comprendre
à un assistant de preuve?", journées francophones des langages
applicatifs (JFLA'04),
26 janvier 2004.
Il y est notamment question de protocoles cryptographiques, de logique,
d'automates d'arbres, et de l'outil H1 (bientôt sur vos écrans!).
Version étendue à SASYFT'2004 (ci-dessous), en anglais.
- L'exposé "On cryptographic protocols,
regular tree languages,
and automated deduction", invité à SASYFT'2004, Orléans, France, 21 juin 2004. Un peu étendu par rapport à celui des JFLA'2004, et en anglais.
- L'exposé "Plate-forme de détection d'intrusions Orchids -
Analyse et corrélation temporelle d'évènements en temps réel",
journées INRIA-industrie 2004, 27 janvier 2004.
- L'exposé "protocoles cryptographiques, analyse de code, détection d'intrusions", séminaire de cryptographie de Rennes, 30 janvier 2004. Un petit survol du précédent et de celui des JFLA, avec en plus l'attaque OpenSSL v2 comme transition habile entre les premier et troisième thèmes de l'exposé. (Où est passé le second? Je n'en ai effectivement pas parlé.)
-
Introduction : ps html.
Exemple : l'appel de méthodes en Java : ps html.
Méthodes formelles et protocoles cryptographiques : ps html. Un protocole dû à Li Gong, avec tentative de modélisation en Prolog, et
modélisé en Coq (exercice : faites la preuve manquante !)
Quelques exercices en Coq : juste les énoncés ou bien avec des solutions; un petit casse-tête à la Lewis Carroll, et une solution possible.
Un exercice déjà un peu plus appliqué: modélisation et spécification du tri par insertion, juste les énoncés ou bien avec des solutions.
Un exercice plus compliqué : l'algorithme d'exclusion mutuelle de Peterson, juste les énoncés ou bien avec des solutions.
L'examen cuvée 1999 : l'énoncé (ps), la solution (ps), et le fichier Coq correspondant.
Le cours des années précédentes :
Les notes de cours, qui commencent à
dater un peu maintenant.
Les règles de déduction utilisées en cours.
Un exemple : le protocole ATMR spécifié en Z.
-
Cours de la filière "preuves" du DEA
Programmation.
Attention: ce cours a assez fortement évolué. Il
consiste cette année en 8 séances portant sur les
thèmes ci-dessous (sauf logiques modales), plus 2 sur la
recherche de preuve en logique linéaire, par Ian Mackie.
|
Cours |
|
Où?
à Paris VII, 175-179 rue du Chevaleret Paris 13ème
(métro Chevaleret)
|
Salle à préciser
|
|
Quand?
|
à partir de début janvier (à préciser)
|
|
Par qui?
|
Jean Goubault-Larrecq
|
|
Ian Mackie |
Notes de cours :
- Logique propositionnelle : ps html;
quelques raffinements de la résolution propositionnelle : ps html;
- Logique classique du premier ordre : ps html;
- Résolution au premier ordre : ps html;
- Tableaux au premier ordre : ps html; Une démonstration de la complétude de LK : ps html;
- Logiques modales : ps html; un texte sur la logique du temps linéaire, traduit à partir du chapitre 4 du livre Nichtklassische Logiken
de Peter H. Schmitt. Contient en particulier l'essentiel de la démonstration du théorème de Kamp.
Examens des années précédentes :
- (1995) Sous-classes de la logique propositionnelle en temps polynomial, énoncé et correction;
- (1996) Unification dans les anneaux booléens, énoncé et correction;
- (1997) La méthode inverse, énoncé et correction;
- (1999) Sous-classes décidables de la logique du premier ordre, énoncé et correction;
- (2000) Résolution dans les clauses avec compteurs, énoncé et correction;
- (2001) Automates alternants généralisés, logique S2S, énoncé et correction;
- (2002) Logique linéaire intuitionniste propositionnelle sans exponentielles, énoncé et correction;