Ces journées sont organisées par le groupe IFSE du RTRA STAE.

Les journées FAC'2017 se sont tenues les 29 et 30 mars à l’ONERA.

Programme des journées :

Mercredi 30 mars

  • 09h00 : accueil

  • 09h30-10h30 : Catherine Dubois, ENSIIE : Interopérabilité des prouveurs : Dedukti, Zenon et FoCaLize à la rescousse.

  • 10h30-11h00 : pause

  • 11h00-12h00 : systèmes distribués

    • Asynchronous Communication Models: a Menagerie of Refinements. Florent Chevrou, Aurélie Hurault, Shin Nakajima, Philippe Quéinnec

    • A study of the Chord protocol using Electrum. Jeanne Tawa, Julien Brunel, David Chemouil

  • 12h00-14h00 : pause

  • 14h-15h30 : validation et vérification

    • Block Library Driven Translation Validation for Dataflow Models in Safety Critical Systems. Arnaud Dieumegard, Adres Toom, Marc Pantel

    • Correct-by-Construction Specification to Verified Code. Ning Ge, Arnaud Dieumegard, Eric Jenn, Laurent Voisin,

    • SMT-Based Synthesis of Fault-Tolerant Architectures. Kevin Delmas, Rémi Delmas, Claire Pagetti,

  • 15h30-16h00 : pause

  • 16h00-17h30 : temps-réel

    • A formal encoding of Clock Constraints Specification Language in Agda : Denotational semantics and Instant refinment. Mathieu Montin, Marc Pantel

    • Outillage pour la modélisation, la vérification et la génération d’applications temporisées et embarquées P.E. Hladik, S. Dal Zilio, O. Pasquier, S. Pillement, B. Berthomieu

    • Distributed Simulation of Heterogeneous and Real-time Systems. Gilles Lasnier, Janette Cardoso, Pierre Siron, Claire Pagetti, Patricia Derler

Jeudi 30 mars

  • 09h30-10h30 : Chantal Keller, LRI, Univ. Paris-Sud : Les prouveurs automatiques pour la preuve et le test formel.

  • 10h30-11h00 : pause

  • 11h00-12h00 : analyses de systèmes

    • Building Confidence on Formal Verification Models. Pierre-Alain Bourdil, Eric Jenn, Silvano Dal Zilio

    • Markov Chain Model of Probabilistic Real-Time Systems. Jasdeep Singh, Luca Santinelli and Guillaume Infantes

  • 12h00-14h00 : pause

  • 14h00-16h00 preuves (session en commun avec le séminaire maths-info du Labex CIMI)

    • Formalization of an existence theorem of Nash equilibrium in Coq and Isabelle. Stéphane Le Roux, Érik Martin Dorel, Jan Georg Smaus

    • A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations. Érik Martin Dorel, Pierre Roux,

    • From signatures to monads in UniMath. Benedikt Ahrens, Ralph Matthes, Anders Mörtberg

    • A temporal Extension of First-Order Logic for Code Analysis. David Come, Julien Brunel, David Doose