Contact

Meeting October 21st, 2021

• Home
• Meetings
• Dissemination
• External Links

Location: AdaCore, 46 rue d'Amsterdam, 75009 Paris

Programme

Les slides seront accessibles dès que possible (merci aux auteurs de me les transmettre).

• 09h30: Welcome coffee
• 10h00: Introduction: the Why3 consortium and the joint laboratory ProofInUse
  Claude Marché
• 10h10: Introduction à Jessie3
  Guillaume Cluzel
• 10h45: Une étude de cas avec Jessie3
  Benjamin Monate
• 11h10: pause
• 11h25: Axes de la collaboration ProofInUse-MERCE, focus sur le Ladder et les contre-exemples
  David Mentré
• 12h00: Colibri2: présentation, focus sur contre-exemples générés
  François Bobot
• 12h35: Lunch break
• 14h00: Trusted Counterexamples in SPARK
  Benedikt Becker
• 14h35: Différentes techniques d'interactions avec l'outil de preuve SPARK
  Yannick Moy
• 15h15: Alt-Ergo et Contre-exemples: présent et futur (discussion)
  Guillaume Bury
• 15h50: pause
• 16h05: Perspectives, discussions diverses
• 17h00: End of meeting

Participants

Sur place:

• Andrei Paskevich, LMF/Toccata
• Benedikt Becker, LMF/Toccata
• Benjamin Monate, TrustInSoft
• Claude Marché, LMF/Toccata
• François Bobot, CEA
• Guillaume Cluzel, LMF/Toccata
• Guillaume Melquiond, LMF/Toccata
• Guillaume Bury, OCamlPro
• Muriel Shan Sei Fan, OCamlPro
• Raphaël Rieu-Helft, TrustInSoft
• Yacine El Haddad, LMF/Toccata
• Yannick Moy, AdaCore

En visio: (connexion sur Google meet)

• Adrien Champion, OCamlPro
• Benoît Boyer, MERCE
• Claire Dross, AdaCore
• David Mentré, MERCE
• Denis Cousineau, MERCE
• Fabrice Le Fessant, OCamlPro
• Florian Faissole, MERCE
• Hichem Ait El Hara, OCamlPro
• Hiroaki Inoue, MERCE
• Jean-Christophe Filliâtre, LMF/Toccata
• Julien Blond, OCamlPro
• Steven De Oliviera, OCamlPro