Programme

The full proceedings are available here.

June 3, 2014

  • 08:45 - 09:00 Registration
  • 09:00 - 10:00 Invited talk
    E. Omodeo. Proof Verification within Set Theory: Exploiting a New Way of Modeling Graphs (PDF)
  • 10:00 - 10:30 Coffee Break
  • 10:30 - 11:05 T. Lecomte. Return of Experience on Automating Refinement in B (PDF)
  • 11:05 - 11:40 P. Halmagrand. Using Deduction Modulo in Set Theory (PDF)
  • 11:40-12:15 G. Rossi. Programming with Partially Specified Collections (PDF)
  • 12:30-14:00 Lunch
  • 14:00-15:00 Invited talk
    D. Pastre. Mathematical Theorem Proving, from Muscadet0 to Muscadet4, Why and How (PDF)
  • 15:00 - 15:35 S. Krings, M. Leuschel, J. Bendisposto. Turning Failure into Proof: Evaluating the ProB Disprover (PDF)
  • 15:35 - 16:00 Coffee Break
  • 16:00 - 16:35 D. Deharbe, P. Fontaine, Y. Guyot, F. Voisin. Introduction to the Integration of SMT-Solvers in Rodin (PDF)
  • 16:35 - 17:10 M. Cristia, G. Rossi. Rapid Prototyping and Animation of Z Specifications Using {log} (PDF)
  • 17:10-17:20 Closing session