La XXVII° édition des journées FAC a eu lieu les 1 et 2 avril prochain à l’ISAE,
(10, avenue Édouard-Belin, Toulouse).

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é Paul Sabatier.

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