meeting -- November 25, 26 2009 -- Paris

Participants

Michaël Armand, Frédéric Besson, Diego Caminha, Pierre-Emmanuel Cornilleau, Germain Faure, Pascal Fontaine, Benjamin Grégoire, Thomas Jensen, Pierre Letouzey, Assia Mahboubi, Stephan Merz, Loïc Pottier, Virgile Prevosto, Laurent Théry, Laurent Voisin.

Program

25 Novembre : Proof format for SMT solvers (livrable D7)
26 Novembre : new combination methods and strategies
  • synthèse proof format for SMT solvers (F.Besson)
  • livrable D2 -- présentation des nouvelles fonctionalités des outils Alt-Ergo et VeriT
  • livrable D3 -- new combination methods
  • livrable D5 -- strategies for efficient deductions
      Work Package 2
  • vue d'ensemble WP 2 (F. Besson)
  • Tâche 5 -- Integrating decision procedures into proof assistants (Sophia)
  • Tâche 6 -- Integrating decision procedures into PCC (Rennes)
  • Tâche 7 -- Integrating decision procedures into Rodin (Systerel)
  • Tâche 8 -- Integrating decision procedures into Frama-C (CEA)
  • Divers