English version

Guillaume Melquiond

Je suis directeur de recherche Inria dans l'équipe Toccata au sein du laboratoire LMF (Université Paris Saclay).

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 CoqInterval. 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. CoqInterval 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 visait 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)

Livres, chapitres de livre et thèse :

• Formal verification for numerical computations, and the other way around.
  HDR et soutenance. HAL, BIB.
• Handbook of Floating-Point Arithmetic (2ème édition), sous la direction de Jean-Michel Muller,
  publié chez Birkhäuser (2018). Résumé. DOI, BIB.
• Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System, avec Sylvie Boldo,
  publié chez ISTE Press - Elsevier (2017). URL, BIB.
• Arithmétique des ordinateurs et preuves formelles, avec Sylvie Boldo,
  dans Informatique Mathématique : une photographie en 2013. BIB.
• Handbook of Floating-Point Arithmetic, sous la direction de Jean-Michel Muller,
  publié chez Birkhäuser (2010). Résumé. DOI, BIB.
• Arithmétique d'intervalles et certification de programmes.
  Thèse (en français) et soutenance. HAL, BIB.

Journaux :

• Enabling floating-point arithmetic in the Coq proof assistant, avec Érik Martin-Dorel et Pierre Roux,
  dans Journal of Automated Reasoning (2023, volume 67). Article. HAL, DOI, BIB.
• Floating-point arithmetic, avec Sylvie Boldo, Claude-Pierre Jeannerod et Jean-Michel Muller,
  dans Acta Numerica (2023, volume 32). Article. HAL, DOI, BIB.
• A strong call-by-need calculus, avec Thibaut Balabonski et Antoine Lanco,
  dans Logical Methods in Computer Science (2023, volume 19.1). Article. HAL, DOI, BIB.
• WhyMP, a formally verified arbitrary-precision integer library, avec Raphaël Rieu-Helft,
  dans Journal of Symbolic Computation (2023, volume 115). Article. HAL, DOI, BIB.
• Formally verified approximations of definite integrals, avec Assia Mahboubi et Thomas Sibut-Pinote,
  dans Journal of Automated Reasoning (2019, volume 62.2). Article. HAL, DOI, BIB.
• Proving tight bounds on univariate expressions with elementary functions in Coq, avec Érik Martin-Dorel,
  dans Journal of Automated Reasoning (2016, volume 57.3). Article. HAL, DOI, BIB.
• Formalization of real analysis: a survey of proof assistants and libraries, avec Sylvie Boldo et Catherine Lelay,
  dans Mathematical Structures in Computer Science (2016, volume 26.7). Article. HAL, DOI, BIB.
• 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. HAL, DOI, BIB.
• 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. HAL, DOI, BIB.
• 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. HAL, DOI, BIB.
• Some issues related to double rounding, avec Érik Martin-Dorel et Jean-Michel Muller,
  dans BIT Numerical Mathematics (2013, volume 53.4). Article. HAL, DOI, BIB.
• 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. HAL, DOI, BIB.
• 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. HAL, DOI, BIB.
• Floating-point arithmetic in the Coq system,
  dans Information and Computation (2012, volume 216). Article. HAL, DOI, BIB.
• 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. HAL, DOI, BIB.
• Certification of bounds on expressions involving rounded operators, avec Marc Daumas,
  dans Transactions on Mathematical Software (2010, volume 37.1). Article. HAL, DOI, BIB.
• 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. HAL, DOI, BIB.
• 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. HAL, DOI, BIB.
• Formally certified floating-point filters for homogeneous geometric predicate, avec Sylvain Pion,
  dans Theoretical Informatics and Applications (2007, volume 41.1). Article. HAL, DOI, BIB.
• The design of the Boost interval arithmetic library, avec Hervé Brönnimann et Sylvain Pion,
  dans Theoretical Computer Science (2006, volume 351). Article. HAL, DOI, BIB.

Conférences :

• Turning the Coq proof assistant into a pocket calculator,
  pour la 15ème édition du Coq WS (2024, Tbilisi, Géorgie). HAL, BIB.
• End-to-end formal verification of a fast and accurate floating-point approximation, avec Florian Faissole et Paul Geneau de Lamarlière,
  pour la 15ème édition de ITP (2024, Tbilisi, Géorgie). HAL, DOI, BIB.
• A safe low-level language for computer algebra and its formally verified compiler, avec Josué Moreau,
  pour la 29ème édition de ICFP (2024, Milan, Italie). HAL, DOI, BIB.
• Slimmer formal proofs for mathematical libraries, avec Paul Geneau de Lamarlière et Florian Faissole,
  pour la 30ème édition d'ARITH (2023, Portland, OR, USA). Article. HAL, BIB.
• Manifest termination, avec Assia Mahboubi,
  pour la 29ème édition de TYPES (2023, Valence, Espagne). Article et exposé. HAL, BIB.
• A strong call-by-need calculus, avec Thibaut Balabonski et Antoine Lanco,
  pour la 6ème édition de FSCD (2021). Article. HAL, DOI, BIB.
• Some formal tools for computer arithmetic: Flocq and Gappa, avec Sylvie Boldo,
  pour la 28ème édition d'ARITH (2021). Article et exposé. HAL, BIB.
• Plotting in a formally verified way,
  pour la 6ème édition de F-IDE (2021). Article et exposé. HAL, DOI, BIB.
• WhyMP, a formally verified arbitrary-precision integer library, avec Raphaël Rieu-Helft,
  pour la 45ème édition d'ISSAC (2020, Kalamata, Grèce). Article. HAL, DOI, BIB.
• Formal verification of a state-of-the-art integer square root, avec Raphaël Rieu-Helft,
  pour la 26ème édition d'ARITH (2019, Kyoto, Japon). Article. HAL, DOI, BIB.
• A Why3 framework for reflection proofs and its application to GMP's algorithms, avec Raphaël Rieu-Helft,
  pour la 9ème édition d'IJCAR (2018, Oxford, Grande-Bretagne). Article. HAL, DOI, BIB.
• A three-tier strategy for reasoning about floating-point numbers in SMT, avec Sylvain Conchon, Mohamed Iguernelala, Kailiang Ji et Clément Fumex,
  pour la 29ème édition de CAV (2017, Heidelberg, Allemagne). Article. HAL, DOI, BIB.
• How to get an efficient yet verified arbitrary-precision integer library, avec Raphaël Rieu-Helft et Claude Marché,
  pour la 9ème édition de VSTTE (2017, Heidelberg, Allemagne). Article. HAL, DOI, BIB.
• Formally verified approximations of definite integrals, avec Assia Mahboubi et Thomas Sibut-Pinote,
  pour la 7ème édition d'ITP (2016, Nancy, France). Article. HAL, DOI, BIB.
• 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. HAL, DOI, BIB.
• 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. HAL, DOI, BIB.
• 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é. HAL, DOI, BIB.
• 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. HAL, DOI, BIB.
• 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. HAL, BIB.
• 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. HAL, DOI, BIB.
• 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. HAL, BIB.
• 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é. HAL, DOI, BIB.
• 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. HAL, DOI, BIB.
• 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é. HAL, DOI, BIB.
• Proving bounds on real-valued functions with computations,
  pour la 4ème édition d'IJCAR (2008, Sidney, Australie). Article et exposé. HAL, DOI, BIB.
• Floating-point arithmetic in the Coq system,
  pour la 8ème édition de RNC (2008, Saint-Jacques de Compostelle, Espagne). Article et exposé. HAL, BIB.
• 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é. BIB.
• 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é. BIB.
• Assisted verification of elementary functions using Gappa, avec Florent de Dinechin et Christoph Lauter,
  pour SAC'06 (2006, Dijon, France). Article et version longue. BIB.
• When double rounding is odd, avec Sylvie Boldo,
  pour la 17ème édition d'IMACS (2005, Paris, France). Article et exposé. HAL, BIB.
• Formal certification of arithmetic filters for geometric predicates, avec Sylvain Pion,
  pour la 17ème édition d'IMACS (2005, Paris, France). Article et exposé. HAL, BIB.
• 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é. HAL, DOI, BIB.
• 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é. HAL, BIB.
• The Boost interval library, avec Hervé Brönnimann et Sylvain Pion,
  pour la 5ème édition de RNC (2003, Lyon, France). Article et exposé. HAL, BIB.

Exposés invités :

• Arithmétique des ordinateurs et preuve formelle,
  pour la 30ème édition des JFLA (2019, Les Rousses, France). Article et exposé.
• 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. BIB.
• 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. BIB.
• Bool_set: multi-valued logic, avec Hervé Brönnimann et Sylvain Pion,
  auprès du comité de normalisation de langage C++ (2006). Rapport technique. BIB.

Développements logiciels

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

Projets et financements

• Fresco (ERC 101001995).
• NuSCAP (ANR-20-CE48-0014).
• FastRelax (ANR-14-CE25-0018).
• Soprano (ANR-14-CE28-0020).
• Verasco (ANR-11-INSE-03).
• Coquelicot (RTRA Digiteo et conseil régional d'Île-de-France).
• FOST (ANR-08-BLAN-0246).

Pour me contacter

Autres ressources

• Google Scholar
• Orcid
• Ohloh