Programme Scientifique EJC'99

---

[EJC'99] [Programme Scientifique] [Inscription] [ Logistique] [ Affiche] [Contacts] [Soutiens]

---

Lundi 22 Mars

Accueil

Logique et Programmation

• programme,
• fonction,
• calcul,
• raisonnement,
• langage.

Mardi 23 Mars

Raisonnement, calcul et formalisation des mathématiques

• logique du premier ordre,
• déduction modulo,
• formalisation des mathématiques,
• théorie des types simples,
• théorie des ensembles,
• symboles lieurs.

Théorie des Types

• langages de programmation,
• lambda-calcul,
• démonstration,
• interprétation de Heyting-Kolmogorov,
• isomorphisme de Curry-Howard,
• spécification.

Mercredi 24 Mars

Méthodes formelles et sécurité

• Introduction,
• Les méthodes formelles
• Domaines d'applications
• Les principales méthodes formelles pour la sécurité
• Les concepts des bases en sécurité (biens, faiblesses, menaces, attaques, cryptographie, ...)
• Politiques et modèles de sécurité
• Les propriétés de sécurités de base
• Les évaluations sécuritaires et l'utilisation de méthodes formelles (ITSEC, TCSEC, CC)
• Vérification de protocoles cryptographique (protocoles d'authentification, protocoles de commerce électronique).

Jeudi 25 Mars

Programmation et vérification des systèmes réactifs

• Programmation
  • Définition des systèmes réactifs
  • Modèles sémantiques de la réactivité
  • Synchronisme et asynchronisme
  • Exemples de langages réactifs : synchrone et asynchrone :
    • ESTEREL
    • ELECTRE
  • Liens entre synchronisme et asynchronisme
  • Modélisation des aspects temporels
• Vérification
  • Objectifs de la vérification
  • Expressions des proprités en logique temporelle
  • Algorithmes de Model Checking
  • Vérifications qualitatives
  • Vérifications quantitatives

Vendredi 26 Mars

Logique et Contraintes

• Logique et Calcul
• Programmation Logique
• Programmation Logique avec contraintes
• Exemples de langages CLP : Herbrand, Réels, Entiers, Contraintes ensemblistes
• Compilation
• Contraintes et concurrence.

• What is Oz? An Introduction
• How to write a Problem Solver in Oz
• Propagate and Enumerate
• Finite Domain Constraints
• Techniques of Constraint Programming
• Scheduling in Oz by Example

Lundi 29 Mars

Sous-types et programmation à objets

• La programmation à objets
  • objets, passage de message, classes, héritage
  • dispatch simple
  • problèmes de typage
  • dispatch multiples et multi-méthodes
• Sous-typage
  • lambda-calcul simplement typé avec sous-typage
  • modèle à enregistrement
  • modèle à surcharge
  • méthodes binaires: le problème de la co-variance
  • perte d'information: polymorphisme et quantification bornée
  • langages à délégation

Mardi 30 Mars

Introduction à la Cryptographie à clé publique

La Cryptographie à clé publique a été inventée en 1976. Elle utilise de jolis résultats d'Algèbre, de théorie des nombres, de logique, et/ou de théorie de la complexité pour résoudre des problèmes qui semblaient auparavant impossibles. Par exemple comment jouer à pile ou face ou au poker par téléphone (sans que l'on puisse tricher), comment savoir lequel de deux milliardaires est le plus riche sans qu'ils aient à révéler leur fortune, ou comment prouver que l'on détient un secret sans le révéler. Nous présenterons surtout les principales applications de la cryptographie à clé publique c.-à.-d. les concepts de chiffrement, signature, et authentification à clé publique. Comme exemple d'algorithmes, nous verrons le RSA, l'algorithme de Rabin et un algorithme "Zero-Knowledge". Suivant le temps, les connaissances, et l'intéret du public nous développerons plus une direction ou une autre !

Mercredi 31 Mars

Systèmes de démonstration automatisée (I)

• Introduction générale aux systèmes de démonstration automatisée.
• Le démonstrateur de Boyer-Moore, Nqthm.
  Le but de ce cours est de donner une vue synthétique des possibilités offertes par ce démonstrateur. On présentera successivement:
  • les principes fondamentaux sous-jacents (principe du shell, principe de définition, principe d'induction)
  • les mécanismes de preuve, illustrés sur un exemple simple
  • les principales aides ("hints") à la preuve
  • un résumé des applications réalisées avec cet outil dans divers domaines.
• Introduction à l'assistant à la démonstration Coq. Le but du cours est de montrer sur des exemples concrets l'application de Coq au développement de programmes corrects. On montrera en particulier la représentation de structures de données, de fonctions récursives et de prédicats. Au cours de la présentation, nous mettrons en évidence les possibilités offertes par le langage et l'architecture de Coq par rapport à d'autres environnements. Nous discuterons en particulier de la manière d'intégrer des procédures de recherche automatique de preuve.

Jeudi 1 Avril

Systèmes de démonstration automatisée (II)

• Introduction à PVS
  • Analyse des spécifications utilisant PVS: On considère comme exemple "l'annuaire electronique".
    • version simple
    • version utilisant les ensembles
    • version qui maintient un invariant
    • résumé
  • PVS
    • Introduction à PVS : créer une spécification PVS, analyse, typechecking, preuve
    • Le langage de spécification de PVS : un exemple simple, un autre un peu compliqué, utilisation des théories, récursion, types dépendants, types abstraits
    • PVS proof checker: utilisation via commandes, procédures de décision, utilisation des définitions et lemmes
    • Des exemples

Approches conceptuelles et pratiques de B (I)

• aborder les concepts mathématiques fondamentaux et les résultats correspondants, qui sous-tendent B.

Vendredi 2 Avril

Approches conceptuelles et pratiques de B (II)

• montrer comment ces concepts peuvent être mis en oeuvre pour:
  • construire un langage formel (mais pratique) doté d'une sémantique claire et
  • construire des outils en accord avec cette sémantique,
• présenter des applications pratiques non-triviales dans le but d'illustrer les deux points précédents.