Sites Inria

Forum Méthodes Formelles 2014

Preuve de modèle, preuve de programme

Cockpit Airbus A350 © Airbus

Le Forum Méthodes Formelles est un cycle de conférences créé par le pôle Aerospace Valley afin de sensibiliser les entreprises aux méthodes formelles pour la conception de systèmes et de logiciels sûrs, en diffusant l'expérience acquise en ce domaine par les grands acteurs de l'aéronautique et de l'espace.

  • Date : 4/02/2014
  • Lieu : Grand amphithéâtre Inria Grenoble
  • Organisateur(s) : Cette conférence est organisée par Aerospace Valley et Minalogic, et accueillie par Inria Grenoble Rhône-Alpes.

Le 4 février 2014 aura lieu la 3ème journée du Forum Méthodes Formelles, un cycle de conférences à l'intention d'un public industriel et académique.

Il s'agit d'un événement unique en France, dont l'objectif est de faire progresser la qualité des logiciels et de leurs méthodes et outils de développement et de vérification, en lien avec des applications concrètes.

Cette 3ème journée sera consacrée aux techniques de preuve, avec des intervenants d'Airbus, ATOS, CEA, CNES, Dassault, Inria, IRIT, LRI, SYSTEREL, TIMA et TrustInSoft.

Cet événement est une retransmission en direct de la conférence qui a lieu au LAAS-CNRS à Toulouse.

Horaires : 8h45 - 17h30

Programme

  • Christine Paulin : « Les langages de preuve »
  • Yamine Ait Ameur : « Introduction large à B »
  • Mathieu Clabaut : « Application critique développée en B »
  • Xavier Leroy : « Introduction large à Coq »
  • Xavier Leroy et Jean Souyris : « Compilateur formellement prouvé : CompCert »
  • Laurence Pierre : « Outils de démonstration automatique et preuve de circuits électroniques »
  • Florent Kirchner et Benjamin Monate : « Présentation de FRAMA-C »
  • Stéphane Duprat : « Preuve unitaire d’un logiciel avionique »
  • Stéphane Duprat et Gregory Navarro : « Vérification par preuve formelle de logiciel de vol spatial »
  • Emmanuel Ledinot : « La preuve au service de la précision de l'Interprétation Abstraite »
  • Table ronde : « De l’utilité de l’abstraction dans la preuve, passage à l’échelle ? »

Retrouvez le programme détaillé

Localisation

Mots-clés : Minalogic Preuve Méthodes formelles Aerospace Valley Systèmes critiques

Haut de page

Suivez Inria tout au long de son 50e anniversaire et au-delà !