La XXX° édition des journées FAC aura lieu les 2 et 3 avril 2025 à l’ISAE, en collaboration avec l’ONERA.
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 26 mars via le formulaire suivant.
https://www.laas.fr/fr/formulaires/fac2025/
Conférenciers invités
Cette année nos conférenciers invités sont:
- 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.
- 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.
Programme
Programme disponible rapidement
Comité de programme
Jean-Paul Bodeveix, Jean-Baptiste Raclet, Quentin Peyras, Marc Pantel, Philippe Quéinnec, Aurélie Hurault, Pascal Sotin, Iulian Ober, Christophe Garion, Célia Picard, David Chemouil, Pierre Roux, Nicolas Amat, Julien Brunel, Clément Foucher, Tomasz Kloda, Didier Le Botlan.