Forum Méthodes Formelles Cycle de conférences

" Preuve de modèle, preuve de programme "

Mardi 04 Février 2014 Salle de Conférences LAAS-CNRS Plan d'accès

Retransmis en direct au Grand amphithéâtre Inria Grenoble en lien avec INRIA et Minalogic.

Programme

• 08h45 -09H00 Accueil des participants
  
  
• 09h00-10h00 Introduction Vidéo
  • « Courte introduction de la journée » slides
    Agusti Canals (CS Communication & Systèmes)
  • « Les langages de preuve » slides
    Christine Paulin (LRI/Univ. Paris Sud)
  
  
• 10h00-11h15 Apports de B au développement formel Vidéo
  • « Introduction large à B » slides
    Yamine Ait Ameur (IRIT/N7 Toulouse)
  • « Application critique développée en B » slides
    Mathieu Clabaut (SYSTEREL)
  
  
• 11h15 -11h30 : Pause Café
  
  
• 11h30-12h50 Développement formel avec Coq Vidéo
  • « Introduction large à Coq » slides
    Xavier Leroy (Inria)
  • « Compilateur formellement prouvé : CompCert » slides
    Xavier Leroy (Inria) et Jean Souyris (Airbus)
  
  
• 12h50-14h00 Repas
  
  
• 14h00-14h45
  • « Outils de démonstration automatique et preuve de circuits électroniques » Vidéo
    Laurence Pierre (TIMA/UJF Grenoble) slides
  
  
  
• 14h45-16h00 Frama C pour la preuve de programme Vidéo
  • « Présentation de l’outil » slides
    Florent Kirchner (CEA) et Benjamin Monate (TrustInSoft)
  • Exemple d’application industrielle chez Airbus :
    « Preuve unitaire d’un logiciel avionique » slides
    Stéphane Duprat (ATOS)
  • Exemple d’application industrielle au CNES :
    « Vérification par preuve formelle de logiciel de vol spatial » slides
    Stéphane Duprat (ATOS) et Gregory Navarro (CNES)
  • Exemple d’application industrielle chez Dassault :
    « La preuve au service de la précision de l'Interprétation Abstraite »
     Emmanuel Ledinot (Dassault)
  
  
• 16h00-16h15 Présentations des Sponsors Vidéo : ATOS , CS , RATP , SYSTEREL
  
• 16h15-16h30 Pause café
  
  
• 16h30-17h30 : Table Ronde animée par Laurence Pierre (TIMA) Vidéo /slides /notes
  « De l’utilité de l’abstraction dans la preuve, passage à l’échelle ? »

Sponsors de la Journée

home