meeting -- June 23, 24 2009 -- Paris

Participants

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

Program

mardi 23 Juin : journée procédure de décision arithmétique
Session assistants de preuve

• Bibliothèques numériques Coq ( Pierre L)
• Micromega et extensions (Frédéric B)

Déjeuner
Session mises en oeuvre de procédures de décision

• SAT modulo linear arithmetic (Germain F)
• Mise en oeuvre d'un simplexe exact (Diego C)
• Certificats pour simplexe flottant (Frédéric B)
• Discussions

24 Juin : Journée plénière

• Compte rendu de la journée précédente (Frédéric B)
• Présentation des benchmarks (20mins par site)
• Suite de présentations des benchmarks (20mins par site)
• Finalisation du délivrable pour la tâche Requirement Analysis
• Structures de données combinées avec des contraintes arithmétiques (Christophe R & Pascal F)
• Certificats pour SAT (Mickael A)
• Discussion tâche Proof witnesses