L'équipe Certilab

Spécifications Formelles, Certification de Logiciel

L'objectif de notre équipe est de développer des méthodes et des bibliothèques de spécifications et de preuves dans le domaine de la certification de logiciel. Une présentation détaillée de nos objectifs est disponible ici.

Les membres de l'équipe:

• Chercheurs:
  • Joëlle Despeyroux (responsable scientifique)
  • André Hirschowitz, Université de Nice (collaborateur exterieur)
  
  
• Doctorants:
  • Guillaume Gillard, ATER à Nantes
  
  
• Secrétariat:
  • Nathalie Bellesso
    
  
  
• Anciens doctorants:
  • Pierre Leleu, chef du Service Études et Grands Travaux à la Direction Départementale de l'Équipement de Seine-Maritime, à Rouen (LeleuP@wanadoo.fr)
  • Delphine Kaplan-Terrasse, enseignante à Eurecom
  
  

Membres du site TYPES à l'INRIA Sophia Antipolis:

• INRIA Sophia Antipolis: Gilles Barthe, Yves Bertot, Joëlle Despeyroux, André Hirschowitz, Loïc Pottier, Laurent Thery, Laurent Chicli, Guillaume Gillard, Hanane Naciri, Simão de Sousa,
• Site associé: Minho, Portugal: Luis Pinto, Maria Joao Frade, Jose Bacelar Almeida, Jose Espirito Santo, Tarmo Uustalu, Olivier Pons and Jorge Sousa Pinto,
• Site industriel: Dassault-Aviation: Emmanuel Ledinot.

Événements à noter:

• Issue spéciale du "Journal of Functional Programming"; sujet: "Logical Frameworks and Meta-languages". La date limite de soumission était le 23 octobre 2000.
• Événements passés:
  • LFM'00. Le "workshop" sur les "Logical Frameworks and Meta-languages" s'est tenu le 25 juin 2000, à Santa Barbara en Californie.
  • Types'99. L'école d'été "Types" a eu lieu sur la Côte d'azur, en France, du 30 aout au 10 septembre 1999.

Enseignement:

• Nous donnons des cours de DEA sur les méthodes formelles et fiabilité du logiciel au Dea d'informatique, à l'université de Nice Sophia-Antipolis (UNSA). Module de tronc commun, 1er cours en automne 2000.
  Ce cours est une partie d'un cours proposé pour un "Mastère" sur le même sujet: " méthodes formelles et fiabilité du logiciel", toujours à l'université de Nice.
• Nous donnons des cours de DEA sur la mécanisation des preuves au Dea d'informatique, à l'université de Nice Sophia-Antipolis (UNSA) (module optionnel).
• Nous avons donné des cours de DEA "Semantique Naturelle: Spécifications et Preuves", au Dea MDFI ("Mathématiques Discrètes et Fondements de l'Informatique") de Marseille, de 1995 à 1999; notes de cours, 80 pages.
  Nouveau cours depuis 99-00: mécanisation des preuves (résumé), variante du cours proposé à Nice.

Les stages dans l'équipe.

Quelques photos de conférences ou écoles d'été.

La page Certilab Inria.