Forum Méthodes Formelles

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.

Le Forum Méthodes Formelles est organisé par les pôles de compétitivité Aerospace Valley et Minalogic. Il a lieu au LAAS-CNRS (Toulouse) et est retransmis en direct dans le grand amphitéâtre Inria Grenoble Rhône-Alpes, de 8h45 à 17h30.

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.

Au 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 ? »

 Programme détaillé : http://projects.laas.fr/IFSE/FMF/J3/index.html

 L’entrée est gratuite mais l’inscription est obligatoire afin de permettre à Minalogic de prévoir les repas et les pauses cafés.
Pour s’inscrire : http://minalogic.insight-outside.fr/inscriptions/index.php Remplir le formulaire puis cliquer sur "S’inscrire à un autre événement", puis sélectionner FMF