La XXIX° édition des journées FAC aura lieu les 3 et 4 avril 2024 au LAAS-CNRS.

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.

Programme des journées

Mercredi 3 avril

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

  • 09h30-10h30 : Invited talk.

    Laurent Mounier (Vérimag, Univ. Grenoble): Vérification formelle pour la détection et l’analyse de vulnérabilités logicielles

La place prépondérante prise par les technologies du numérique dans notre quotidien s’accompagne d’une augmentation croissante - en nombre et en degré de sophistication - des cyberattaques auxquelles nous devons faire face. L’une des causes de ces attaques réside dans des erreurs de conception et/ou de développement des logiciels que nous utilisons, des systèmes d’exploitation aux logiciels applicatifs. Détecter et analyser la dangerosité de ces vulnérabilités est donc un enjeu majeur pour les développeurs/intégrateurs de logiciels, pour les organismes de certification et pour la mise en place de correctifs et mécanismes de protections adéquats.

Pour cela il est nécessaire de disposer d’outils permettant d’automatiser certaines analyses de code spécifiques à la sécurité. Nous présenterons comment l’utilisation de techniques de vérification formelle dédiées permet de répondre à ce besoin en l’illustrant notamment à travers deux exemples d’attaques “avancées”, les attaques par injection de fautes et les attaques dites adaptatives.

10h30-11h00 : pause

  • 11h00-12h15 : session “theorem proving”

    • Modeling bigraphs with Coq. Cécile Marcon, Cyril Allignol, Celia Picard and Xavier Thirioux
    • Democratic Forking and Isabelle/HOL. Jan-Georg Smaus
    • Enabling Floating-Point Arithmetic in the Coq Proof Assistant. Érik Martin-Dorel, Guillaume Melquiond and Pierre Roux   (J. Autom. Reason.)

12h15-13h45 : repas

  • 13h45-15h00 : session “Robotics and Unmaned Systems”

    • A Formal Framework for the Specification, Verification and Validation of Robotic Skills Composition for Autonomous Mission Design. Baptiste Pelletier, Charles Lesire, Karen Godary-Dejean, David Doose, Christophe Grand and Mathieu Rognant

    • ProSkill: A formal skill language for acting in robotics. Felix Ingrand   (preprint)

    • UAS procedures model with system architecture for safety analysis. Charles Mathou, Kevin Delmas, Pierre de Saqui-Sannes and Jean-Charles Chaudemar   (SysCon2023)

15h00-15h30 : pause

  • 15h30-16h45 : session “Formal Models, Scheduling”

    • Towards Verifying Security Policies for Infinite-state Systems. Quentin Peyras, Ghada Gharbi and Souheib Baarir
    • A Verification Algorithm relying on First-Order Buchi Automata. Quentin Peyras, Julien Brunel and David Chemouil
    • High Multiplicity RCPSP with Compound Activities and Learning Effect. Duc Anh Le, Stéphanie Roussel, Anouck Chan and Christophe Lecoutre   (ROADEF2024)

Jeudi 4 avril

  • 09h30-10h30 : Invited Talk

    Caterina Urban (INRIA Paris, équipe ANTIQUE et ENS): Machine Learning Interpretability and Verification

Machine learning (ML) software is increasingly being employed in high stakes or sensitive applications. This brings forth important challenges related to safety, privacy, and non-discrimination. As a consequence, research in ML verification rapidly gained popularity and demand for interpretable ML models is more and more pronounced. Interpretability and verification are typically seen as orthogonal concerns. Research in ML interpretability is predominantly carried out in the ML community, while research in ML verification is almost exclusively carried out in the formal methods community, without much communication and exchanges between these research areas. In this talk, we advocate for closing this gap by highlighting the synergies between interpretability and verification in ML software. We will survey our recent and ongoing work, and discuss research questions and avenues for future work in this context.

10h30-11h00 : pause

  • 11h00-12h15 : session “Formal Verification”

    • Project and Conquer: Fast Quantifier Elimination for Checking Petri Nets Reachability. Nicolas Amat, Silvano Dal Zilio and Didier Le Botlan   (VMCAI2024)
    • Automated Polyhedral Abstraction Proving. Nicolas Amat, Silvano Dal Zilio and Didier Le Botlan   (PetriNets2023)
    • Towards Automatic Detection of Deadlocks in SCOOP. Bertrand Meyer   (preprint)

12h15-13h45 : repas

  • 13h45-15h00 : session “Formal Verification”

    • Formal verification of a fault-tolerant MAC-based hardware accelerator with SMT. Anthony Faure-Gignoux, Kevin Delmas, Adrien Gauffriau and Claire Pagetti
    • Verification for Object Detection - IBP IoU. Noémie Cohen, Mélanie Ducoffe, Ryma Boumazouza, Christophe Gabreau, Claire Pagetti, Xavier Pucel and Audrey Galametz   (preprint)
    • Towards proved formal specification and verification of STL operators as synchronous observers. Céline Bellanger, Pierre-Loic Garoche, Matthieu Martel and Célia Picard   (FMAS2023)

14h45-15h15 : pause

  • 15h15-16h30 : session “event-B”

    • From Event-B to Lambdapi. Anne Grieu
    • Formalising Liveness Properties in Event-B with the Reflexive EB4EB Framework. Peter Riviere, Neeraj Singh, Yamine Ait Ameur and Guillaume Dupont   (NFM2023)

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.