La XXVIII° édition des journées FAC a eu lieu les 5 et 6 avril 2023 à l’ISAE.

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, de l’ONERA et de l’Université Toulouse III, Paul Sabatier.

Programme des journées

Mercredi 5 avril

09h00 : accueil présentation des journées

  • 09h30-10h30 : Invited talk.

Mathieu Martel : (LAMPS, Univ. Perpignan) Matrix Computations: In Seek of Frugality

Frugal computing is becoming an important topic for environmental reasons. In this context, several techniques have been proposed to reduce the storage of scientific data by dedicated compression methods specially tailored for arrays of floating-point numbers. While these techniques are quite efficient to save memory, they introduce additional computations to com- press and decompress data before processing them. In this article, we introduce a new lossy, fixed-rate compression technique for 2D-arrays of floating-point numbers which allows one to compute directly on the compressed data, without decompressing them. We obtain important speedups since less operations are needed to compute among the compressed data and since no decompression and re-compression is needed. More precisely, our technique makes it possible to perform basic linear algebra operations such as addition, multiplication by a constant among compressed matrices and dot product and matrix multiplication among partly uncompressed matrices. This work has been implemented into a tool named blaz and we present a comparison with the well- known compressor zfp in terms of execution-time and accuracy.

10h30-11h00 : pause

  • 11h00-12h15 : session “méthodes déductives”

    • Containers for Specification in SPARK. Claire Dross   (HILT 2022)
    • Property Directed Reachability for Generalized Petri Nets. Nicolas Amat, Silvano Dal Zilio and Thomas Hujsa   (TACAS 2022)
    • Formal verification of an anti-collision algorithm for autonomous vehicles. Guerric Chupin and Xavier Jean

12h15-13h45 : repas

  • 13h45-15h00 : session “systèmes embarqués”

    • Fault injection strategies: identifying HW failures with functional impact. Iban Guinebert, Andres Barrilado, Kevin Delmas, Franck Galtié and Claire Pagetti
    • How to conciliate critical embedded systems with asynchronous programming? Émilie Thomé
    • Predictive Runtime Verification of Skill-based Robotic Systems using Petri Nets. Baptiste Pelletier, Charles Lesire, Christophe Grand, David Doose and Mathieu Rognant

15h00-15h30 : pause

  • 15h30-16h45 : session “temps-réel”

    • Configuration of Guard Band and Offsets in Cyclic Queuing and Forwarding. Damien Guidolin-Pina, Marc Boyer and Jean-Yves Le Boudec
    • Critical pairs based diagnosability analysis of timed fault in Time Petri Nets. Camille Coquand, Audine Subias, Yannick Pencolé and Eric Lubat   (WODES 2022)
    • Formalization of Requirements for Correct Systems. Imen Sayar and Jeanine Souquières   (FormReq 2020)

Jeudi 6 avril

  • 09h30-10h30 : Invited Talk

    Jean-Christophe Filliâtre (LMF, Univ. Paris-Saclay): Why3, une plateforme pour la vérification déductive

Dans cet exposé, nous présentons l’outil Why3, une plateforme pour la vérification déductive de programmes développée au Laboratoire Méthodes Formelles (Université Paris-Saclay, CNRS, ENS Paris-Saclay / Inria Saclay). Cette plateforme est utilisée dans les milieux académiques et industriels pour la vérification d’algorithmes, de codes écrits dans langages tels que C, Ada ou OCaml, ou encore la vérification de protocoles cryptographiques. La plateforme Why3 est également exploitée pour enseigner la vérification de programmes. Cet exposé met en avant les atouts de la plateforme Why3 et décrit le cœur de métier de son équipe de développement.

10h30-11h00 : pause

  • 11h00-12h15 : session “model checking”

    • Verifying temporal relational models with Pardinus. Nuno Macedo, Julien Brunel, David Chemouil and Alcino Cunha
    • A Verified UAV Flight Plan Generator. Baptiste Pollien, Christophe Garion, Gautier Hattenberger, Pierre Roux and Xavier Thirioux   (FormaliSE 2023)
    • POPiX: A Fixed-Point Code Synthesis Tool Based on Constraint Generation. Dorra Ben Khalifa   (DASIP 2022)

12h15-13h45 : repas

  • 13h45-15h30 : session “theorem proving”

    • Towards the formalisation of interactive properties. Cécile Marcon, Celia Picard, Cyril Allignol and Xavier Thirioux
    • Democratic forking: An application of interactive theorem proving to game theory. Jan-Georg Smaus
    • A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant. Pierre Pomeret-Coquot, Hélène Fargier and Érik Martin-Dorel

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.