Guillaume Melquiond

I am an INRIA researcher in the Proval team from the LRI (Université Paris Sud).

My research interests are floating-point and interval arithmetic, and formal proof. I am working on methods for formally certifying the correctness (behavior and accuracy) of numerical applications; these methods are implemented in the Gappa tool. I am also working on using numerical computations for formally proving mathematical theorems; there is now a library of tactics for the Coq proof assistant.

Publications (bibtex)

Book and PhD thesis:

• Handbook of Floating-Point Arithmetic, coordinated by Jean-Michel Muller,
  published by Birkhäuser. Summary.
• Arithmétique d'intervalles et certification de programmes.
  Thesis (in French) and defense.

Journals:

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

Conferences:

• Combining Coq and Gappa for certifying floating-point programs,
  with Sylvie Boldo and Jean-Christophe Filliâtre,
  for the 16th Calculemus symposium (2009, Grand Bend, ON, Canada). Paper and talk.
• Proving bounds on real-valued functions with computations,
  for the 4th IJCAR symposium (2008, Sidney, Australia). Paper and talk.
• Floating-point arithmetic in the Coq system,
  for the 8th RNC symposium (2008, Santiago de Compostela, Spain). Paper and talk.
• Proposing Interval Arithmetic for the C++ Standard, with Hervé Brönnimann and Sylvain Pion,
  for the 12th SCAN symposium (2006, Duisburg, Germany). Talk.
• Proof and certification for an accurate discriminant, with Sylvie Boldo and Marc Daumas and William Kahan,
  for the 12th SCAN symposium (2006, Duisburg, Germany). Talk.
• Assisted verification of elementary functions using Gappa, with Florent de Dinechin and Christoph Lauter,
  for the SAC'06 symposium (2006, Dijon, France). Paper and extended paper.
• When double rounding is odd, with Sylvie Boldo,
  for the 17th IMACS symposium (2005, Paris, France). Paper and talk.
• Formal certification of arithmetic filters for geometric predicates, with Sylvain Pion,
  for the 17th IMACS symposium (2005, Paris, France). Paper and talk.
• Guaranteed proofs using interval arithmetic, with Marc Daumas and César Muñoz,
  for the 17th Arith symposium (2005, Cape Cod, MA, USA). Paper and talk.
• Generating formally certified bounds on values and round-off errors, with Marc Daumas,
  for the 6th RNC symposium (2004, Schloß Dagstuhl, Germany). Paper and talk.
• The Boost interval library, with Hervé Brönnimann and Sylvain Pion,
  for the 5th RNC symposium (2003, Lyon, France). Paper and talk.

Some reports:

• IEEE interval standard working group - P1788: current status, with William Edmonson,
  for the 19th Arith symposium (2009, Portland, OR, USA). Paper and talk (first part).
• Directed rounding arithmetic operations, with Sylvain Pion,
  for the C++ standardization committee (2009). Technical report.
• A Proposal to add Interval Arithmetic to the C++ Standard Library, with Hervé Brönnimann and Sylvain Pion,
  for the C++ standardization committee (2006). Technical report.
• Bool_set: multi-valued logic, with Hervé Brönnimann and Sylvain Pion,
  for the C++ standardization committee (2006). Technical report.

Software contributions

• Library of Coq tactics for proving inequalities on real-valued expressions.
• Gappa formal tool for certifying numerical applications.
• Contributor to Why and Frama-C.
• Maintainer of the interval arithmetic library of Boost.

Contact information

Last update: January 7th, 2010.