La XXX° édition des journées FAC aura lieu les 2 et 3 avril 2025 à l’ISAE, en collaboration avec l’ONERA.
Ces journées sont organisées par le groupe IFSE du RTRA STAE avec un soutien spécial de l’ENAC, l’INSA Toulouse, ISAE-Supaero, l’ONERA, Toulouse-INP et de l’Université Toulouse III, Paul Sabatier.
La participation est gratuite. Pensez à vous inscrire.
Vous pouvez aussi trouver comment se rendre à l’ISAE.
Mercredi 2 avril
09h00 : accueil et présentation des journées
-
09h30-10h30 : Invited talk.
Stefania Dumbrava (SAMOVAR et ENSIIE, équipe ACMES): Reliable Graph Data Processing at Scale: Challenges and Opportunities
Property graphs are widely used in applications handling interconnected, heterogeneous data, yet their schema definition remains less understood than in relational databases, posing challenges for data integrity. This talk first presents recent advances in specifying and discovering graph schema constraints and their role in improving database robustness. We then explore how schema-aware graph transformations can enhance the reliability of graph database applications, particularly through greybox fuzzing techniques that leverage code coverage feedback to generate more effective test inputs. Finally, we discuss key challenges in balancing availability, consistency, and constraint preservation at scale, highlighting open problems and future directions.
10h30-11h00 : pause
-
11h00-12h30 : session “modélisation et vérification”
-
BiCoq : Bigraphs Formalisation with Coq. Cécile Marcon, Cyril Allignol, Celia Picard, Blair Archibald, Michele Sevegnani and Xavier Thirioux. (SAC 2025)
-
Contribution to the Verification of Complex Graphical Equations Using Z3. Ali Ben Taouet and Daniel Prun.
-
GRust: A Programming Language for Automotive Engineering. Émilie Thomé and Christine Tasson.
-
12h30-14h00 : repas
-
14h00-15h30 : session “systèmes robotiques”
-
Skill-Based Architectures in Autonomous Systems: An Empirical Study. Pierre Malafosse, Alexandre Albore, Jérémie Guiochet and Charles Lesire. (IFM 2024)
-
Combining Offline and Online Formal Verification of ROS2 Node. Sylvain Raïs, Julien Brunel, David Doose and Frédéric Herbreteau.
-
A formal implementation of Behavior Trees to act in robotics. Felix Ingrand.
-
15h30-16h00 : pause
-
16h00-17h00 : session “analyse de systèmes hardware”
-
A Statistical Approach to Capturing an Application’s Footprint on GPU. Cédric Cazanove, Benjamin Lesage, Frédéric Boniol and Jérôme Ermont.
-
A Reactive System-specific Compilation Chain from Synchronous Dataflow Models to FPGA Netlist. Inès Winandy, Pierre-Loic Garoche, Arnaud Dion and Florent Manni. (SMC-IT 2024)
-
Jeudi 3 avril
-
09h30-10h30 : Invited Talk
Frédéric Herbreteau (LaBRI et Bordeaux-INP, équipe MTV): Finite abstractions for the verification of (concurrent) timed automata
Timed automata are a commonly used model for verifying real-time systems. They extend finite automata by introducing clock variables, which allow for expressing constraints on the timing of events during a run. As these variables take values from non-negative real numbers, the state-space of timed automata is uncountably large. Formal verification algorithms use a finite symbolic representation of this state-space, called a zone graph. The finiteness of the zone graph is guaranteed through finite abstractions that preserve the properties being verified. We introduce the state-of-the-art abstraction, aLU, and demonstrate how it can be applied in verification algorithms in order to ensure termination.
In the second part, we focus on concurrent timed automata, where multiple timed processes (automata) interact with one another. In the typical global-time semantics, time progresses synchronously across all processes. We propose an alternative local-time semantics, where each process operates on its own timeline. We identify conditions under which the local-time semantics is equivalent to the global-time semantics. Additionally, we show that the local-time semantics has desirable properties, leading to a more compact state-space representation compared to the global-time approach. As with the global-time case, the finiteness of the zone graph in the local-time model relies on abstraction techniques. However, preserving certain properties is more complex in the local-time setting. We present solutions to adapt the aLU abstraction for use with local-time semantics.
10h30-11h00 : pause
-
11h00-12h30 : session “analyse de systèmes hardware”
-
Formally Verified Hardening of C Programs against Hardware Fault Injection. Basile Pesin, Sylvain Boulmé, David Monniaux and Marie-Laure Potet. (CPP 2025)
-
Modelling and proving the monotonicity of processor pipelines in Coq. Alban Gruin, Armelle Bonenfant, Thomas Carle, Christine Rochange. (MEMOCODE 2024)
-
Optimisation of Reasoning over Ontologies on Embedded Hardware for Avionics-Context Semantic-Aware to Generate Minimisation of Computation Time and Memory Footprint. Youssef Amari. (ESWC 2024)
-
12h30-14h00 : repas
-
14h00-15h00 : session “méthodes formelles”
-
Encoding TLA+ proof obligations safely for SMT. Rosalie Defourné. (ABZ 2024)
-
Translating Event-B models and proofs to TLA+. Anne Grieu, Jean-Paul Bodeveix and Mamoun Filali.
-
15h00-15h30 : pause
-
15h30-16h30 : session “réseaux de neurones”
-
Efficient Implementation of Neural Networks Usual Layers on Fixed-Point Architectures. Dorra Ben Khalifa and Matthieu Martel. (LCTES 2024)
-
Verification of neural network mechanisms for ACAS-Xu systems. Martin Boniol, Christophe Garion, Julien Brunel, Xavier Thirioux and Jean-Baptiste Chaudron.
-
Comité de programme
Jean-Paul Bodeveix, Julien Brunel, Silvano Dal Zilio, Mamoun Filali, Christophe Garion, Didier Le Botlan, Iulian Ober, Marc Pantel, Célia Picard, Philippe Quéinnec, Jean-Baptiste Raclet, Pierre Roux, Matthieu Roy, Pascal Sotin.