Guillaume Melquiond

Je suis chargé de recherche INRIA dans l'équipe Proval au LRI (Université Paris Sud).

Mes travaux de recherche tournent autour des arithmétiques à virgule flottante et d'intervalles et de la preuve formelle. Je m'intéresse d'une part à la certification formelle de programmes numériques (correction du comportement, précision des résultats), ce qui a donné l'outil Gappa. Je m'intéresse d'autre part à l'utilisation de calculs numériques pour effectuer la preuve de théorèmes mathématiques, ce qui a donné une bibliothèque de tactiques pour l'assistant de preuves Coq. Pour finir, je développe Flocq, une formalisation générique de l'arithmétique à virgule flottante en Coq.

Si vous voulez un aperçu de ce que j'ai fait ces dernières années, vous pouvez jeter un œil à mon aide-mémoire.

Publications (bibtex)

Livre et thèse :

• Handbook of Floating-Point Arithmetic, sous la direction de Jean-Michel Muller,
  publié chez Birkhäuser. Résumé.
• Arithmétique d'intervalles et certification de programmes.
  Document (en français) et soutenance.

Journaux :

• Certifying the floating-point implementation of an elementary function using Gappa, avec Florent de Dinechin et Christoph Lauter,
  dans Transactions on Computers (2011, volume 60.2). Article.
• Certification of bounds on expressions involving rounded operators, avec Marc Daumas,
  dans Transactions on Mathematical Software (2010, volume 37.1). Article.
• Computing predecessor and successor in rounding to nearest, avec Sylvie Boldo, Siegfried Rump et Paul Zimmermann,
  dans BIT Numerical Mathematics (2009, volume 49.2). Article.
• Emulation of FMA and correctly-rounded sums: proved algorithm using rounding to odd, avec Sylvie Boldo,
  dans Transactions on Computers (2008, volume 57.4). Article.
• Formally certified floating-point filters for homogeneous geometric predicate, avec Sylvain Pion,
  dans Theoretical Informatics and Applications (2007, volume 41.1). Article.
• The design of the Boost interval arithmetic library, avec Hervé Brönnimann et Sylvain Pion,
  dans Theoretical Computer Science (2006, volume 351). Article.

Conférences :

• Flocq: a unified library for proving floating-point algorithms in Coq, avec Sylvie Boldo,
  pour la 20ème édition d'ARITH (2011, Tübingen, Allemagne). Article et exposé.
• Formal proof of a wave equation resolution scheme: the method error, avec Sylvie Boldo, François Clément, Micaela Mayero, Jean-Christophe Filliâtre et Pierre Weis,
  pour la 1ère édition de ITP (2010, Edinburgh, Écosse). Article.
• Combining Coq and Gappa for certifying floating-point programs, avec Sylvie Boldo et Jean-Christophe Filliâtre,
  pour la 16ème édition de Calculemus (2009, Grand Bend, ON, Canada). Article et exposé.
• Proving bounds on real-valued functions with computations,
  pour la 4ème édition de IJCAR (2008, Sidney, Australie). Article et exposé.
• Floating-point arithmetic in the Coq system,
  pour la 8ème édition de RNC (2008, Saint-Jacques de Compostelle, Espagne). Article et exposé.
• Proposing Interval Arithmetic for the C++ Standard, avec Hervé Brönnimann et Sylvain Pion,
  pour la 12ème édition de SCAN (2006, Duisburg, Allemagne). Exposé.
• Proof and certification for an accurate discriminant, avec Sylvie Boldo, Marc Daumas et William Kahan,
  pour la 12ème édition de SCAN (2006, Duisburg, Allemagne). Exposé.
• Assisted verification of elementary functions using Gappa, avec Florent de Dinechin et Christoph Lauter,
  pour SAC'06 (2006, Dijon, France). Article et version longue.
• When double rounding is odd, avec Sylvie Boldo,
  pour la 17ème édition de IMACS (2005, Paris, France). Article et exposé.
• Formal certification of arithmetic filters for geometric predicates, avec Sylvain Pion,
  pour la 17ème édition de IMACS (2005, Paris, France). Article et exposé.
• Guaranteed proofs using interval arithmetic, avec Marc Daumas et César Muñoz,
  pour la 17ème édition de ARITH (2005, Cape Cod, MA, États-Unis). Article et exposé.
• Generating formally certified bounds on values and round-off errors, avec Marc Daumas,
  pour la 6ème édition de RNC (2004, Schloß Dagstuhl, Allemagne). Article et exposé.
• The Boost interval library, avec Hervé Brönnimann et Sylvain Pion,
  pour la 5ème édition de RNC (2003, Lyon, France). Article et exposé.

Rapports divers :

• IEEE interval standard working group - P1788: current status, avec William Edmonson,
  pour la 19ème édition de Arith (2009, Portland, OR, États-Unis). Article et exposé (première partie).
• Directed rounding arithmetic operations, avec Sylvain Pion,
  auprès du comité de normalisation du langage C++ (2009). Rapport technique.
• A Proposal to add Interval Arithmetic to the C++ Standard Library, avec Hervé Brönnimann et Sylvain Pion,
  auprès du comité de normalisation de langage C++ (2006). Rapport technique.
• Bool_set: multi-valued logic, avec Hervé Brönnimann et Sylvain Pion,
  auprès du comité de normalisation de langage C++ (2006). Rapport technique.

Contributions logicielles

• Bibliothèque de tactiques Coq pour la preuve d'inégalités sur des expressions réelles.
• Formalisation Flocq de l'arithmétique à virgule flottante en Coq : bases, formats et précisions quelconques.
• Outil Gappa d'aide à la certification formelle de programmes numériques.
• Participation à Why et Frama-C.
• Participation à Boost et mainteneur de la bibliothèque d'arithmétique par intervalles.

Pour me contacter

Pour finir, voici quelques liens.

Dernière mise à jour : 19 août 2011.