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)

• Présentation de la tache (F. Besson)
• Format de preuve de veriT (P. Fontaine)
• Format de preuve pour SAT (M.Armand)
• Format de preuve pour pour EUF et arithmétique (F.Besson & P-E Cornilleau)
• Discussions

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