English version

Guillaume Melquiond

Je suis chargé de recherche Inria dans l'équipe Toccata / VALS au LRI (Université Paris Sud).

Thèmes de recherche

Mes travaux de recherche se placent à la frontière de l'arithmétique des ordinateurs et de la preuve formelle.

• Preuve automatique de propriétés numériques. Je m'intéresse aux méthodes permettant d'automatiser la vérification de programmes numériques. En particulier, je développe l'outil Gappa et la bibliothèque Coq.Interval. Gappa est dédié à la preuve formelle de fonctions courtes mais compliquées utilisant l'arithmétique à virgule flottante  on retrouve de telles fonctions dans des bibliothèques mathématiques comme CRlibm. Coq.Interval fournit des tactiques Coq permettant de prouver formellement des inégalités sur des expressions à valeurs réelles par le calcul. Enfin, je regarde du côté de prouveurs SMT comme Alt-Ergo afin d'améliorer leur support des arithmétiques réelle et à virgule flottante.
• Vérification formelle de programmes. En matière de preuve de programme, je participe aussi à des projets de plus grande ampleur. Ainsi le but du projet FOST était de réaliser la preuve formelle complète d'un programme de calcul d'analyse numérique résolvant l'équation des ondes. Le projet Verasco vise quant à lui à développer un compilateur C et des outils d'analyse statique formellement vérifiés. Enfin, je participe au développement de l'architecture Why3 de vérification déductive de programmes et à ses interactions avec les systèmes Coq et Gappa.
• Formalisation de l'arithmétique. Les sujets précédents nécessitent que les assistants de preuve supportent l'arithmétique réelle, l'analyse et l'arithmétique à virgule flottante. Je participe ainsi aux projets Coquelicot et Flocq. Coquelicot est une extension conservative de la bibliothèque standard de Coq sur les réels tandis que Flocq est une formalisation générique de l'arithmétique à virgule flottante en Coq.
• Arithmétique par intervalles. Indépendamment des systèmes formels, je m'intéresse aux calculs robustes sur ordinateur et en particulier à l'arithmétique par intervalles. J'ai ainsi participé au développement d'une bibliothèque C++ générique pour Boost. Je suis aussi membre du comité IEEE 1788 pour la normalisation de l'arithmétique par intervalles et je m'intéresse aux évolutions du langage C++ en faveur du calcul scientifique.

Publications (bibtex)

Livre, chapitre de livre et thèse :

• Arithmétique des ordinateurs et preuves formelles, avec Sylvie Boldo,
  dans Informatique Mathématique : une photographie en 2013.
• Handbook of Floating-Point Arithmetic, sous la direction de Jean-Michel Muller,
  publié chez Birkhäuser (2010). Résumé. DOI.
• Arithmétique d'intervalles et certification de programmes.
  Document (en français) et soutenance.

Journaux :

• Coquelicot: a user-friendly library of real analysis for Coq, avec Sylvie Boldo et Catherine Lelay,
  dans Mathematics in Computer Science (2015, volume 9.1). Article. DOI.
• Verified compilation of floating-point computations, avec Sylvie Boldo, Jacques-Henri Jourdan et Xavier Leroy,
  dans Journal of Automated Reasoning (2015, volume 54.2). Article. DOI.
• Formalization of real analysis: a survey of proof assistants and libraries, avec Sylvie Boldo et Catherine Lelay,
  dans Mathematical Structures in Computer Science (2014). Article. DOI.
• Trusting computations: a mechanized proof from partial differential equations to actual program, avec Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero et Pierre Weis,
  dans Computers & Mathematics with Applications (2014, volume 68.3). Article. DOI.
• Some issues related to double rounding, avec Érik Martin-Dorel et Jean-Michel Muller,
  dans BIT Numerical Mathematics (2013, volume 53.4). Article. DOI.
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program, avec Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero et Pierre Weis,
  dans Journal of Automated Reasoning (2013, volume 50.4). Article. DOI.
• Numerical approximation of the Masser-Gramain constant to four decimal digits: δ = 1.819..., avec W. Georg Nowak et Paul Zimmermann,
  dans Mathematics of Computation (2013, volume 82). Article. DOI.
• Floating-point arithmetic in the Coq system,
  dans Information and Computation (2012, volume 216). Article. DOI.
• 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. DOI.
• Certification of bounds on expressions involving rounded operators, avec Marc Daumas,
  dans Transactions on Mathematical Software (2010, volume 37.1). Article. DOI.
• 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. DOI.
• 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. DOI.
• Formally certified floating-point filters for homogeneous geometric predicate, avec Sylvain Pion,
  dans Theoretical Informatics and Applications (2007, volume 41.1). Article. DOI.
• The design of the Boost interval arithmetic library, avec Hervé Brönnimann et Sylvain Pion,
  dans Theoretical Computer Science (2006, volume 351). Article. DOI.

Conférences :

• Inductive verification of hybrid automata with strongest postcondition calculus, avec Daisuke Ishii et Shin Nakajima,
  pour la 10ème édition d'iFM (2013, Turku, Finlande). Article. DOI.
• Preserving user proofs across specification changes, avec François Bobot, Jean-Christophe Filliâtre, Claude Marché et Andrei Paskevich,
  pour la 5ème édition de VSTTE (2013, Menlo Park, CA, USA). Article. DOI.
• A formally-verified C compiler supporting floating-point arithmetic, avec Sylvie Boldo, Jacques-Henri Jourdan et Xavier Leroy,
  pour la 21ème édition d'ARITH (2013, Austin, TX, USA). Article et exposé. DOI.
• Improving real analysis in Coq: a user-friendly approach to integrals and derivatives, avec Sylvie Boldo et Catherine Lelay,
  pour la 2nde édition de CPP (2012, Kyoto, Japon). Article. DOI.
• Built-in treatment of an axiomatic floating-point theory for SMT solvers, avec Sylvain Conchon, Cody Roux et Mohamed Iguernelala,
  pour la 10ème édition du SMT Workshop (2012, Manchester, UK). Article.
• A Simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic, avec François Bobot, Sylvain Conchon, Évelyne Contejean, Mohamed Iguernelala, Assia Mahboubi et Alain Mebsout,
  pour la 6ème édition d'IJCAR (2012, Manchester, UK). Article. DOI.
• Différentiabilité et intégrabilité en Coq. Application à la formule de d'Alembert, avec Catherine Lelay,
  pour la 23ème édition des JFLA (2012, Carnac, France). Article.
• 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é. DOI.
• Formal proof of a wave equation resolution scheme: the method error, avec Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero et Pierre Weis,
  pour la 1ère édition de ITP (2010, Edinburgh, Écosse). Article. DOI.
• 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é. DOI.
• Proving bounds on real-valued functions with computations,
  pour la 4ème édition d'IJCAR (2008, Sidney, Australie). Article et exposé. DOI.
• 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 d'IMACS (2005, Paris, France). Article et exposé.
• Formal certification of arithmetic filters for geometric predicates, avec Sylvain Pion,
  pour la 17ème édition d'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 d'ARITH (2005, Cape Cod, MA, États-Unis). Article et exposé. DOI.
• 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é.

Exposés invités :

• Formal verification of a floating-point elementary function,
  pour les tutoriels de la 22ème édition d'ARITH (2015, Lyon, France). Exposé.
• Automating the verification of floating-point algorithms,
  pour la 12ème édition de SMT (2014, Vienne, Autriche). Exposé.
• Automated methods for verifying floating-point algorithms,
  pour MSC (2014, Lyon, France). Exposé.
• Automations for verifying floating-point algorithms,
  pour la 5ème édition de Coq (2013, Rennes, France). Exposé.
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program,
  pour CaCoS (2012, Grenoble, France). Exposé.
• Numerical computations and formal methods,
  pour la 3ème édition des RAIM (2009, Lyon, France). Exposé.
• IEEE interval standard working group - P1788: current status, avec William Edmonson,
  pour la 19ème édition d'ARITH (2009, Portland, OR, États-Unis). Article et exposé (première partie). DOI.

Rapports divers :

• 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.

Développements logiciels

• Gappa : outil d'aide à la vérification formelle de programmes numériques.
• Coq.Interval : tactiques pour la preuve d'inégalités sur des expressions réelles en Coq.
• Flocq : formalisation Coq de l'arithmétique à virgule flottante en bases, formats et précisions quelconques.
• Why3 : architecture de vérification logicielle.
• Coquelicot : formalisation de l'analyse réelle en Coq facile d'utilisation.
• Boost.Interval : bibliothèque C++ générique d'arithmétique par intervalle.
• Remake : une variante minimaliste de make qui supporte les dépendances dynamiques.
• Quelques contributions mineures à Why, Frama-C et Coq.

Projets et financements

• FastRelax (ANR).
• Soprano (ANR).
• Verasco (ANR-11-INSE-03).
• Coquelicot (RTRA Digiteo et conseil régional d'Île-de-France).
• FOST (ANR-08-BLAN-0246-01).

Pour me contacter

Autres ressources

• Google Scholar
• Ohloh