La XXVI° édition des journées FAC aura lieu les 27 et 28 mars prochain à l’IRT Saint Exupéry (bâtiment B612, 3 rue Tarfaya, Toulouse).

Inscriptions.

La participation aux journées est gratuite.

Afin de pouvoir dimensionner correctement les pauses-café et les repas, il est demandé de s’inscrire au plus tard le mardi 19 mars via le formulaire suivant:

Conférenciers invités

Cette année nos conférenciers invités seront:

Satisfiability Modulo Theories (SMT) solvers are increasingly used in verification as back-ends to check the satisfiability of formulas in presence of interpreted symbols. After a brief overview of their architecture, we will review the current methods used in those solvers to handle quantifiers. An early technique, E-matching or trigger-based instantiation, generates instances when some patterns of terms are present in the formula. Although it is experimentally quite successful, it might generate many useless instances. Model-based quantifier instantiation is a more recent semantic instantiation technique: instances are built to fix a tentative model that does not agree with the quantified formulas. An even more recent method to which we have contributed is conflict-based instantiation; it can be seen as a weaker and more efficient form of model-based instantiation, that generates only the instances that contradict the partial model in the ground solver. Finally, we will also report on our results on revisiting enumerative instantiation. These two contributions are joint work with Haniel Barbosa and Andrew Reynolds.

  • Karine Heydemann, (LIP6 / Univ. Pierre et Marie Curie): Attaques en faute: modélisation, sécurisation et analyse de robustesse de code.

Les attaques en faute sur les systèmes embarqués sont puissantes : elles permettent de récupérer des informations sensibles, de contourner des protections, d’escalader des privilèges… S’en prémunir nécessite d’identifier les modèles de faute induits par les moyens d’injection de fautes, de concevoir des protections et de valider la robustesse de ces protections. L’exposé a pour objectif de présenter la problématique et un panorama de l’ensemble de travaux réalisés depuis plusieurs années, au LIP6 et en collaboration avec différents partenaires (académiques et industriels). Certains travaux seront présentés plus en détails. Notamment la première partie de l’exposé se concentrera sur la définition de modèle de faute à partir d’expérimentations réelles par injection d’impulsion électromagnétique. La deuxième partie de l’exposé concernera la conception de schéma de protections, notamment un mis en oeuvre à la compilation. Enfin, l’exposé se terminera par la présentation de l’outil RobustB permettant d’analyser la robustesse de code binaire soumis à des fautes. La conclusion présentera des perspectives et questions ouvertes.

Programme

Mercredi 27 mars

  • 09h00 : accueil présentation des journées et actualités du chantier IFSE par Marc Pantel

  • 09h30-10h30 : Karine Heydemann, (LIP6 / Univ. Pierre et Marie Curie): Attaques en faute: modélisation, sécurisation et analyse de robustesse de code.

  • 10h30-11h00 : pause

  • 11h00-12h30 :

    • Petri Net Reductions for Counting Markings. Bernard Berthomieu , Didier Le Botlan , Silvano Dal Zilio

    • Analysis and Synthesis of Weighted Marked Graph Petri Nets. Raymond R. Devillers, Thomas Hujsa

    • Revisiting Bounded Reachability Analysis of Timed Automata Based on MILP. Iulian Ober

  • 12h30-14h00 : repas

  • 14h-15h30 :

    • Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm. Guillaume Davy, Eric Feron, Pierre-Loic Garoche and Didier Henrion

    • Convergence and covering on graphs for wait-free robots. Armando Castañeda, Sergio Rajsbaum, Matthieu Roy

    • On the Impact of Numerical Accuracy Optimization on General Performances of Programs. Nasrine Damouche

  • 15h30-16h00 : pause

  • 16h00-17h30 :

    • Formal Verification of the Functional Layer of Robotic and Autonomous Systems. Mohammed Foughali

    • Event-B formalization of a variability-aware component model patterns framework. Jean-Paul Bodeveix, Arnaud Dieumegard, Mamoun Filali

    • Model Based System Engineering for Co-Simulation in Extended Enterprise. Renan Leroux, Marc Pantel, Ileana Ober, Jean-Michel Bruel

Jeudi 28 mars

  • 09h30-10h30 : Pascal Fontaine, (LORIA / INRIA & Univ. Lorraine): Quantifiers and SMT.

  • 10h30-11h00 : pause

  • 11h00-12h30 :

    • Identification of multi-core interference. Frédéric Boniol, Claire Pagetti and Nathanaël Sensfelder

    • Modeling Cache Coherence to Expose Interference. Nathanael Sensfelder, Julien Brunel, et Claire Pagetti

    • Towards the qualification of an AADL model transformation tool with contracts. Christophe Garion, Jérôme Hugues et Guillaume Brau

  • 12h30-14h00 : repas

  • 14h-15h30 :

    • Reasoning about Database Queries and Updates. Mohamed Chaabani, Rachid Echahed, Martin Strecker

    • A Bounded Model Property for a Pragmatic Fragment of First-Order Linear Temporal Logic. Quentin Peyras, Julien Brunel, David Chemouil

    • Proof-Based Approach for Hybrid Systems Development using Event-B. Guillaume Dupont, Yamine Ait Ameur, Marc Pantel, Neeraj Singh

Comité de programme

Jean-Paul Bodeveix, Mamoun Filali, Jean-Baptiste Raclet, Marc Pantel, Philippe Quéinnec, Pascal Sotin, Iulian Ober, Julien Brunel, Claire Pagetti, Pierre Roux, Silvano Dal Zilio, Pierre-Emmanuel Hladik, Didier Le Botlan, Matthieu Roy, Christophe Garion.