Les journées FAC ont été organisées par le groupe SVF / FéRIA : Spécification, Vérification Formelles.

Les journées FAC'2010 auront lieu les 31 mars et 1er avril 2010, salle du 1er étage du bâtiment d’accueil à l’ONERA.

Préalablement aux journées FAC, José Luiz Fiadeiro a donné un cours intensif de 2 fois 3h le 30 mars sur la théorie des catégories appliquée à l’architecture des logiciels et systèmes.

Programme des journées :

Mercredi 31 mars 2010

  • 9h30 Ouverture des Journées par Bernard Lecussan, Directeur du DTIM

  • 9h45-10h45 Conférencier invité
    Foundations of Service-Oriented Modelling.
    José Luiz Fiadeiro University of Leicester

  • 10h45-11h15 Pause

  • Session 1 : Fondements

    • 11h15-11h45 Calculs sur les attributs dans la réécriture de graphes fondés sur les approches catégoriques et les types inductifs. Bertrand Boisvert, Louis Féraud, Sergei Soloviev IRIT-UPS

    • 11h45-12h15 Categorical Semantics and Non-Free Categories. Antoine El Khoury, Sergei Soloviev, Laurent Mehats, Mark Spivakovsky IRIT-UPS

  • 12h15-14h00 Repas

  • Session 2 : Optimisation (1)

    • 14h00-14h30 Scheduling Analysis under Fault Bursts. Florian Many ONERA-DTIM

    • 14h30-15h00 Collaboration entre méthode d’ordonnancement et calcul réseau. Marc Boyer, David Doose ONERA-DTIM

  • 15h00-15h30 Pause

  • Session 3 : Vérification (1)

    • 15h30-16h00 Verification of the Schorr-Waite algorithm - From trees to graphs. Mathieu Giorgino, Martin Strecker, Ralph Matthes, Marc Pantel IRIT-UPS, IRIT-ENSEEIHT

    • 16h00-16h30 Mixing induction and co-induction in Coq : a case study for lists. Celia Picard, Ralph Matthes IRIT-UPS

Jeudi 1er avril 2010

  • 9h30-10h30 Conférencier invité
    Requirements Engineering: From Craft to Discipline. Axel van Lamsweerde Université catholique de Louvain (UCL)

  • 10h30-11h00 Pause

  • Session 4 : Vérification (2)

    • 11h00-11h30 GraphSeq: a Graph Matching tool for the extraction of mobility patterns. Minh Duc Nguyen, Hélène Waeselynck, Nicolas Rivière LAAS-CNRS

  • Session 5 : Optimisation (2)

    • 11h30-12h00 Estimation de propriétés temporelles de réseaux temps-réel par méthode de Monte Carlo. Cédric Mauclair ONERA-DTIM

    • 12h00-12h30 Assistance à la conception de modèles à l’aide de contraintes. Marie de Roquemaurel, Thomas Polacsek, Jean-François Rolland, Jean-Paul Bodeveix, Mamoun Filali IRIT-UPS, ONERA-DTIM

  • 12h30-14h00 Repas

  • Session 6 : Vérification (3)

    • 14h00-14h30 Hierarchical Set Decision Diagrams and Automatic Saturation. Alexandre Hamez, Yann Thierry-Mieg, Fabrice Kordon LAAS-CNRS, EPITA, LIP6

    • 14h30-15h00 Peg-Solitaire Game: A Benchmark example for State Space Construction Algorithms. Rodrigo T. Saad, Silvano Dal Zilio, Bernard Berthomieu, Francois Vernadat LAAS-CNRS

    • 15h00-15h30 Machine-Checked Sequencer for Critical Embedded Code Generator. Nassima Izerrouken, Marc Pantel, Xavier Thirioux IRIT-ENSEEIHT, Continental Automotive