Table des matières

• L'équipe
• Introduction
• Thèmes de recherche
  • Environnements de preuves
  • Formalisation de théories mathématiques
  • Implémentations certifiées d'algorithmes de calcul scientifique
• Positionnement vis-à-vis des autres projets issus de CROAP
• Insertion dans la communauté scientifique
  • Collaborations effectives
  • Collaborations à développer et contexte
• Relations industrielles
  • Certification de logiciel en Aéronautique
  • Dyade, France
  • Vérilog, France
  • Prover Technology, Suède
• Utilisateurs de nos travaux.
  • Les utilisateurs du système Coq
  • Les industriels
  • Les étudiants et les enseignants
• Applications potentielles
  • Télécommunications
  • Digilog, France
  • Cryptographie
  • Enseignement
• Enseignement, formation, animation
  • DEA MDFI (Marseille/INRIA Sophia)
  • Maîtrise de mathématiques de l'UNSA (MASF, option informatique)
  • Stages
  • Thèses
  • Initiation à la preuve formelle
  • Organisation de conférence
• Programme
  • Thème 1 : Environnements de preuve
  • Thème 2 : Formalisation de théories mathématiques
  • Thème 3 : Implémentations certifiées d'algorithmes
• Objectifs à 3 ans
• Références
• Table des matières