La XXVII° édition des journées FAC devait avoir lieu en avril 2020 à l’ISAE.

Pour raison de crise sanitaire qu’il n’est pas necessaire de préciser, la réunion a dû être annulée. Nous souhaitions néanmoins garder une trace des exposés qui avaient été programmé et remercier chaleureusement nos collègues qui avaient proposé une présentation, ainsi que nos conférenciers invités, Cezara Drăgoi (INRIA & ENS Paris) et Jean-Christophe Filliatre (LRI, Université Paris Sud & CNRS / INRIA Saclay).

Programme des journées:

mercredi 1er avril

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

  • 09h30-10h30 : Cezara Drăgoi, (INRIA & ENS Paris)

  • 10h30-11h00 : pause

  • 11h00-12h30 : session réseaux de Petri

    • Robotic System Specification Methodology Based on Hierarchical Petri Nets. Maksym Figat

    • A State Class Construction for Computing the Intersection of Time Petri Nets Languages. Éric Lubat, Silvano Dal-Zilio, Didier Le Botlan, Yannick Pencolé, Audine Subias

    • Checking marking reachability with the state equation in Petri nets subclasses. T. Hujsa, B. Berthomieu, S. Dal Zilio, D. Le Botlan

  • 12h30-14h00 : repas

  • 14h-15h30 : session langages formels

    • Recursive data structures in SPARK. Claire Dross, Johannes Kanig

    • Djnn/Smala: A Conceptual Framework and a Language for Interaction-Oriented Programming. Mathieu Magnaudet, Stéphane Chatty, Stéphane Conversy, Sébastien Leriche, Célia Picard, Daniel Prun

    • Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol. Jean-Paul Bodeveix, Julien Brunel, David Chemouil, Mamoun Filali

  • 15h30-16h00 : pause

  • 16h00-17h30 : session algèbre/topologie

    • K set-agreement bounds in round-based models: the power of combinatorial topology. Adam Shimi, Armando Castañeda

    • Taylor series revisited. Xavier Thirioux, Alexis Maffart

jeudi 2 avril

  • 09h30-10h30 : Jean-Christophe Filliatre, (LRI, Université Paris Sud & CNRS / INRIA Saclay)

  • 10h30-11h00 : pause

  • 11h00-12h30 : session systèmes de transitions

    • Formal Approach for the Verification of Onboard Autonomous Functions in Observation Satellites. Silvano Dal Zilio, Vincent Mussot, Loïc Correnson, Serge Rainjonneau, Yves Bardout, Grégoire Scano

    • Synthesis of Weighted Marked Graphs from Constrained Labelled Transition Systems: A Geometric Approach. Raymond R. Devillers, Evgeny Erofeev, Thomas Hujsa

    • Single State Trackability of Discrete Event Systems. Valentin Bouziat, Xavier Pucel, Stéphanie Roussel, Louise Travé-Massuyès

  • 12h30-14h00 : repas

  • 14h00-15h30 : session preuve

    • Nash equilibrium in Coq and Isabelle. Jan-Georg Smaus, Erik Martin-Dorel, Stephane Le Roux

    • Certification of Breadth-First Algorithms by Extraction. Dominique Larchey-Wendling, Ralph Matthes

    • Formal Verification of Real-time Networks. Lucien Rakotomalala, Marc Boyer, Pierre Roux

  • 15h30-16h00 : pause

  • 16h00-17h00 : session temps-réel/architecture

    • On How to Identify Cache Coherence: Case of the NXP QorIQ T4240+. Nathanael Sensfelder, Julien Brunel, Claire Pagetti

    • Hippo: a Faithful Real-Time Execution Engine for the Formal Language Fiacre. P.-E. Hladik, S. Dal Zilio, F. Ingrand

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