La XXVII° édition des journées FAC a eu lieu les 14 et 15 octobre 2021 à l’ENAC (bâtiment Bréguet, amphithéâtre Bellonte, 7, avenue Édouard-Belin, Toulouse).

Ces journées sont organisées par le groupe IFSE du RTRA STAE avec un soutien spécial de l’INSA Toulouse, de l’ISAE et de l’ENAC.

Programme des journées

Jeudi 14 octobre

  • 09h00 : accueil présentation des journées

  • 09h30-10h30 : Invited talk.

    Joao Marques-Silva (IRIT, Toulouse): Logic-Based Explainable AI.

The forecast applications of machine learning (ML) in high-risk and safety-critical applications hinge on systems that are robust in their operation and that can be trusted. This talk overviews recent efforts on applying logic-enabled automated reasoning tools in explaining non-interpretable (black-box) ML models. Concretely, the talk details the computation of rigorous explanations of black-box models, and how these serve for assessing the quality of widely used heuristic explanation approaches. The talk also overviews properties relating different kinds of rigorous explanations. Finally, the talk briefly overviews ongoing work on mapping tractable explainability.

  • 10h30-11h00 : pause

  • 11h00-12h30 :

  • Recursive Data Structures in SPARK. Claire Dross and Johannes Kanig   (CAV 2020)

  • Verifying the Mathematical Library of an UAV Autopilot with Frama-C. Baptiste Pollien, Xavier Thirioux, Christophe Garion, Gautier Hattenberger and Pierre Roux   (FMICS 2021)

  • Verification of machine learning based cyber-physical systems: a comparative study. Arthur Clavière, Laura Altieri Sambartolomé, Eric Asselin, Christophe Garion and Claire Pagetti

  • 12h30-14h00 : repas

  • 14h-16h00 :

  • Generic LaSalle Theory and Pattern for Event-B. Marius Hinge, Catherine Dubois and Marc Pantel

  • Verifying min-plus Computations with Coq. Lucien Rakotomalala, Pierre Roux and Marc Boyer   (NFM 2021)

  • Determinacy and Nash Equilibria of Preference Priority Games Proven in Isabelle. Stephane Le Roux, Érik Martin-Dorel and Jan-Georg Smaus   (AAMAS 2021)

  • Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset. Lélio Brun, Bourke Timothy and Marc Pouzet   (POPL 2020)

  • 16h00-16h30 : pause

  • 16h30 : visite du planétarium de l’ENAC (nombre de places limitées)

Vendredi 15 octobre

  • 09h30-10h30 : Invited Talk

    Behçet Açikmeşe (Univ. Washington, Seattle): Optimization Based Control – An Aerospace Perspective.

Many future aerospace engineering applications will require dramatic increases in our existing autonomous control capabilities. These include robotic sample return missions to planets, comets, and asteroids, formation flying spacecraft, swarms of autonomous spacecraft, unmanned aerial, ground, and underwater vehicles, and autonomous commercial robotic applications. A key control challenge for many autonomous systems is to achieve the performance goals safely with minimal resource use in the presence of mission constraints and uncertainties. In principle these problems can be formulated and solved as optimal control problems. The challenge is solving them reliably in real-time, while assuring: i) full utilization of the performance envelope for the autonomous system; ii) systematic verification of the control algorithms. Our approach to solving these challenging control problems is optimization-based control where we formulate these control problems as optimization problems and then to exploit convex optimization theory and algorithms for their robust and numerically efficient solutions.

  • 10h30-11h00 : pause

  • 11h00-12h30 :

  • Formalization of the semantics of a reactive-interactive language: an attempt with bigraphs. Nicolas Nalpon, Cyril Allignol, Blair Archibald, Celia Picard and Michele Sevegnani

  • A statistical study of the multi-phase representation for real-time tasks running in multi-core processors. Rémi Meunier, Thomas Carle and Thierry Monteil

  • Hippo: A Formal-Model Execution Engine to Control and Verify Critical Real-Time Systems. Pierre-Emmanuel Hladik, Felix Ingrand, Silvano Dal Zilio and Reyyan Tekin   (JSS)

  • 12h30-14h00 : repas

  • 14h-15h30 :

  • A New Product Construction for the Diagnosability of Patterns in Time Petri Net. Éric Lubat, Silvano Dal Zilio, Didier Le Botlan, Yannick Pencolé and Audine Subias   (CDC 2020)

  • Model-Based Synthesis of Incremental and Correct Estimators for Discrete Event Systems. Stéphanie Roussel, Xavier Pucel, Valentin Bouziat and Louise Travé-Massuyès   (IJCAI 2020)

  • Sound Verification Procedures of Temporal Properties of FOLTL Specifications. Quentin Peyras, Jean-Paul Bodeveix, Julien Brunel and David Chemouil   (CAV 2021)

  • 15h30-16h00 : pause

  • 16h00-17h30 :

  • On How to Identify Cache Coherence: Case of the NXP QorIQ T4240. Nathanael Sensfelder, Julien Brunel and Claire Pagetti   (ECRTS 2020)

  • On the Combination of Polyhedral Abstraction and SMT-Based Model Checking for Petri Nets. Nicolas Amat, Silvano Dal Zilio and Bernard Berthomieu   (ICATPN 2021)

  • Populating MBSE Models from MDAO Analysis. Ombeline AÏello, David Sanchez Del Rio Kandel, Jean-Charles Chaudemar, Olivier Poitou and Pierre de Saqui-Sannes   (ISSE 2021)

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