Master de sciences et technologies mention : informatique

Acronyme : sacc	Spécialité : STL	3 ECTS	Niveau : 500	Semestre : S3
Titre : Sémantique de la concurrence et de la mobilité
Responsable : Frederic PESCHANSKI		Répartition hebdomadaire ou semestrielle
		(CM: 3h00)
Contenu La concurrence et la mobilité sont des aspects difficiles mais incontournables des systèmes d'information actuels. Ce cours propose une introduction aux concepts sous-jacents des langages dédiés à la modélisation et à la programmation de systemes concurrents et mobiles dans une optique de sûreté de fonctionnement.
Expérience du responsable dans le domaine de l’UE J'étudie la sémantique de la concurrence et de la mobilité depuis mon DEA (systèmes informatiques répartis de Paris 6) et dans le cadre ma thèse de doctorat sur la composition de logiciel concurrent et réparti. Dans le cadre d'un post-doc de deux ans à l'université de Tokyo, j'ai approfondi l'étude des théories de mobilité et notamment le pi-calcul. J'étudie maintenant, en tant que Maître de Conférence à Paris 6, l'application des théories de concurrence et de mobilité dans le cadre des Systèmes Multi-Agents. L'ensemble de ces recherches ont abouti à des publications d'envergure internationale.
Réalisations du responsable dans le domaine de l’UE MobileScope : A Programming Language with Objective Mobility. Frederic Peschanski, Takashi Masuyama, Yoshihiro Ooyama and Akinori Yonezawa. International Journal on Wireless and Mobile Computing, InderScience, à paraître, 2006. Mobile Agents in Interaction Spaces, Foundations of Coordination Languages and Software Architectures, ENTCS, Elsevier, 2005. On Linear Time and Congruence in Channel-passing Calculi. Frederic Peschanski. In Communicating Process Architectures, pp. 39--53, IOS Press. 2004. Les Espaces d'Interaction : vers une Geometrie des Systemes d'Agents Mobiles. F. Peschanski, R. Affeldt et J-P. Briot. Langages et Modèles Objet 2004. RSTI - TSI L'Objet, Mars 2004. When Concurrent Control Meets Functional Requirements, or Z + Petri Nets. F. Peschanski and D. Julien. ZB 2003. LNCS 2651. Springer-Verlag. June 2003.

Acronyme : sct	Spécialité : STL	3 ECTS	Niveau : 500	Semestre : S3
Titre : Spécification et certification en théorie des types
Responsable : Thérèse HARDIN		Répartition hebdomadaire ou semestrielle
		(30h/7 semaines)
Contenu Cette UE a pour objectif l'étude des théories des types qui fondent les langages de spécification formelle et les méthodes de preuve de correction du logiciel. Une place importante est réservée à l'étude des propriétés logiques et mathématiques de ces théories. La manipulation de différents systèmes d'aide à la preuve permet de comprendre leur mise en oeuvre. Enfin, leur utilisation dans les outils de compilation ou d'édition de liens sont aussi présentées.
Expérience du responsable dans le domaine de l’UE Quelques thèmes de recherche de T. Hardin, accompagnés de quelques publications: Compilation et sémantique ( Hardin, Properties of CCL, TCS, 1989, Explicit substitutions properties, Curien, Hardin, Lévy, JACM 1996, Hardin,Maranget, Pagano,Functional runtime systems, J. of Functional Programming, 1998,T. Hardin, Mammass,Proving the Bounded Retransmission Protocol in the Pi-calculus, NFINITY'98 ). Logique et démonstration automatique (Dowek,Hardin,Kirchner, Higher-order unification via explicit substitutions, Information and Computation,2000; Theorem Proving modulo, Journal of Automated Reasoning,2003). Responsable du projet FOCAL, atelier de développement de systèmes répondant aux besoins élevés de sûreté et de sécurité (Dubois,Hardin, Viguié, Building certified components within FOCAL,Trends in Functional Programming,2004; http://focal.inria.fr), utilisé dans 3 ACI Sécurité (Modulogic, Edemoi, Alidecs). Sûreté de fonctionnement (P. Ayrault, T. Hardin, Développement d'un outil d'évaluation de la sûreté du logiciel, JFLA2000, Hardin, Logiciels de confiance, JFLA2002). Quelques thèmes d'enseignement de T. Hardin, correspondant à des cours de niveaux L et M: Programmation (Hardin , V. Viguié-Donzeau, Concepts et outils de programmation, avec Caml et Ada, InterEditions1992), Lambda-calculs, Théorie des types, Réécriture, Sémantiques, démonstration automatique, Sûreté de fonctionnement (Normes, méthodes de mise en oeuvre, méthodes d'évaluation), accent mis sur tous les aspects liés au logiciel embarqué, en particulier sur les méthodes formelles.