I am an Inria researcher in the Toccata team from the LMF laboratory (Université Paris Saclay).

My work lies at the intersection between the domains of computer arithmetic and formal proof.

**Automated proof of numerical properties.**I am interested in methods for automating the verification of numerical programs. In particular, I am developing the Gappa tool and the CoqInterval library. Gappa is dedicated to the formal proof of small yet complicated functions relying on floating-point arithmetic; such functions can be found in mathematical libraries such as CRlibm. CoqInterval provides some Coq tactics for formally proving inequalities on real-valued expressions by performing computations. I am also investigating SMT solvers such as Alt-Ergo in order to improve their support for real and floating-point arithmetics.**Formal verification of programs.**With respect to program proof, I am also participating to bigger projects. For instance, the goal of the FOST project was to achieve a comprehensive formal proof of a scientific computing program that solves the wave equation. The Verasco project aimed at developing and formally verifying a C compiler and some static analysis tools. I am also contributing to the development of the Why3 framework for deductive verification of programs and to its interactions with Coq and Gappa.**Formalization of arithmetic.**The above topics require from proof assistants a good support for real numbers and analysis, and for floating-point arithmetic. As a consequence, I am also part of the Coquelicot and Flocq projects. Coquelicot is a conservative extension of Coq's standard library on real numbers, while Flocq is a generic formalization of floating-point arithmetic in Coq.**Interval arithmetic.**I am also looking at reliable computations outside formal systems, and more precisely at interval arithmetic. For instance, I am one of the developers of a generic interval module for the Boost C++ library. I am also a member of the IEEE 1788 committee for standardizing interval arithmetic and I follow the evolution of the C++ language with respect to support for scientific computations.

`bibtex`

)**Formal verification for numerical computations, and the other way around**.

HDR and defense. HAL, BIB.**Handbook of Floating-Point Arithmetic**(2nd edition), coordinated by Jean-Michel Muller,

published by Birkhäuser (2018). Summary. DOI, BIB.**Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System**, with Sylvie Boldo,

published by ISTE Press - Elsevier (2017). URL, BIB.**Arithmétique des ordinateurs et preuves formelles**, with Sylvie Boldo,

in Informatique Mathématique : une photographie en 2013. BIB.**Handbook of Floating-Point Arithmetic**, coordinated by Jean-Michel Muller,

published by Birkhäuser (2010). Summary. DOI, BIB.**Arithmétique d'intervalles et certification de programmes**.

PhD thesis (in French) and defense. HAL, BIB.

**Enabling floating-point arithmetic in the Coq proof assistant**, with Érik Martin-Dorel and Pierre Roux,

in Journal of Automated Reasoning (2023, volume 67). Paper. HAL, DOI, BIB.**Floating-point arithmetic**, with Sylvie Boldo, Claude-Pierre Jeannerod, and Jean-Michel Muller,

in Acta Numerica (2023, volume 32). Paper. HAL, DOI, BIB.**A strong call-by-need calculus**, with Thibaut Balabonski and Antoine Lanco,

in Logical Methods in Computer Science (2023, volume 19.1). Paper. HAL, DOI, BIB.**WhyMP, a formally verified arbitrary-precision integer library**, with Raphaël Rieu-Helft,

in Journal of Symbolic Computation (2023, volume 115). Paper. HAL, DOI, BIB.**Formally verified approximations of definite integrals**, with Assia Mahboubi and Thomas Sibut-Pinote,

in Journal of Automated Reasoning (2019, volume 62.2). Paper. HAL, DOI, BIB.**Proving tight bounds on univariate expressions with elementary functions in Coq**, with Érik Martin-Dorel,

in Journal of Automated Reasoning (2016, volume 57.3). Paper. HAL, DOI, BIB.**Formalization of real analysis: A survey of proof assistants and libraries**, with Sylvie Boldo and Catherine Lelay,

in Mathematical Structures in Computer Science (2016, volume 26.7). Paper. HAL, DOI, BIB.**Coquelicot: a user-friendly library of real analysis for Coq**, with Sylvie Boldo and Catherine Lelay,

in Mathematics in Computer Science (2015, volume 9.1). Paper. HAL, DOI, BIB.**Verified compilation of floating-point computations**, with Sylvie Boldo, Jacques-Henri Jourdan, and Xavier Leroy,

in Journal of Automated Reasoning (2015, volume 54.2). Paper. HAL, DOI, BIB.**Trusting computations: a mechanized proof from partial differential equations to actual program**, with Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, and Pierre Weis,

in Computers & Mathematics with Applications (2014, volume 68.3). Paper. HAL, DOI, BIB.**Some issues related to double rounding**, with Érik Martin-Dorel and Jean-Michel Muller,

in BIT Numerical Mathematics (2013, volume 53.4). Paper. HAL, DOI, BIB.**Wave equation numerical resolution: a comprehensive mechanized proof of a C program**, with Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, and Pierre Weis,

in Journal of Automated Reasoning (2013, volume 50.4). Paper. HAL, DOI, BIB.**Numerical approximation of the Masser-Gramain constant to four decimal digits: δ = 1.819...**, with W. Georg Nowak and Paul Zimmermann,

in Mathematics of Computation (2013, volume 82). Paper. HAL, DOI, BIB.**Floating-point arithmetic in the Coq system**,

in Information and Computation (2012, volume 216). Paper. HAL, DOI, BIB.**Certifying the floating-point implementation of an elementary function using Gappa**, with Florent de Dinechin and Christoph Lauter,

in Transactions on Computers (2011, volume 60.2). Paper. HAL, DOI, BIB.**Certification of bounds on expressions involving rounded operators**, with Marc Daumas,

in Transactions on Mathematical Software (2010, volume 37.1). Paper. HAL, DOI, BIB.**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. HAL, DOI, BIB.**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. HAL, DOI, BIB.**Formally certified floating-point filters for homogeneous geometric predicate**, with Sylvain Pion,

in Theoretical Informatics and Applications (2007, volume 41.1). Paper. HAL, DOI, BIB.**The design of the Boost interval arithmetic library**, with Hervé Brönnimann and Sylvain Pion,

in Theoretical Computer Science (2006, volume 351). Paper. HAL, DOI, BIB.

**Slimmer formal proofs for mathematical libraries**with Paul Geneau de Lamarlière and Florian Faissole,

for the 30th ARITH symposium (2023). Paper. HAL, BIB.**Manifest termination**, with Assia Mahboubi,

for the 29th TYPES conference (2023, Valencia, Spain). Paper and talk. HAL, BIB.**A strong call-by-need calculus**, with Thibaut Balabonski and Antoine Lanco,

for the 6th FSCD conference (2021). Paper. HAL, DOI, BIB.**Some formal tools for computer arithmetic: Flocq and Gappa**, with Sylvie Boldo,

for the 28th ARITH symposium (2021). Paper and talk. HAL, BIB.**Plotting in a formally verified way**,

for the 6th F-IDE workshop (2021). Paper and talk. HAL, DOI, BIB.**WhyMP, a formally verified arbitrary-precision integer library**, with Raphaël Rieu-Helft,

for the 45th ISSAC symposium (2020, Kalamata, Greece). Paper. HAL, DOI, BIB.**Formal verification of a state-of-the-art integer square root**, with Raphaël Rieu-Helft,

for the 26th ARITH symposium (2019, Kyoto, Japan). Paper. HAL, DOI, BIB.**A Why3 framework for reflection proofs and its application to GMP's algorithms**, with Raphaël Rieu-Helft,

for the 9th IJCAR conference (2018, Oxford, United Kingdom). Paper. HAL, DOI, BIB.**A three-tier strategy for reasoning about floating-point numbers in SMT**, with Sylvain Conchon, Mohamed Iguernelala, Kailiang Ji, and Clément Fumex,

for the 29th CAV conference (2017, Heidelberg, Germany). Paper. HAL, DOI, BIB.**How to get an efficient yet verified arbitrary-precision integer library**, with Raphaël Rieu-Helft and Claude Marché,

for the 9th VSTTE conference (2017, Heidelberg, Germany). Paper. HAL, DOI, BIB.**Formally verified approximations of definite integrals**, with Assia Mahboubi and Thomas Sibut-Pinote,

for the 7th ITP symposium (2016, Nancy, France). Paper. HAL, DOI, BIB.**Inductive verification of hybrid automata with strongest postcondition calculus**, with Daisuke Ishii and Shin Nakajima,

for the 10th iFM symposium (2013, Turku, Finland). Paper. HAL, DOI, BIB.**Preserving user proofs across specification changes**, with François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich,

for the 5th VSTTE conference (2013, Menlo Park, CA, USA). Paper. HAL, DOI, BIB.**A formally-verified C compiler supporting floating-point arithmetic**, with Sylvie Boldo, Jacques-Henri Jourdan, and Xavier Leroy,

for the 21st ARITH symposium (2013, Austin, TX, USA). Paper and talk. HAL, DOI, BIB.**Improving real analysis in Coq: a user-friendly approach to integrals and derivatives**, with Sylvie Boldo and Catherine Lelay,

for the 2nd CPP symposium (2012, Kyoto, Japan). Paper. HAL, DOI, BIB.**Built-in treatment of an axiomatic floating-point theory for SMT solvers**, with Sylvain Conchon, Cody Roux, and Mohamed Iguernelala,

for the 10th SMT workshop (2012, Manchester, UK). Paper. HAL, BIB.**A Simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic**, with François Bobot, Sylvain Conchon, Évelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, and Alain Mebsout,

for the 6th IJCAR symposium (2012, Manchester, UK). Paper. HAL, DOI, BIB.**Différentiabilité et intégrabilité en Coq. Application à la formule de d'Alembert**, with Catherine Lelay,

for the 23th JFLA meeting (2012, Carnac, France). Paper. HAL, BIB.**Flocq: a unified library for proving floating-point algorithms in Coq**, with Sylvie Boldo,

for the 20th ARITH symposium (2011, Tübingen, Germany). Paper and talk. HAL, DOI, BIB.**Formal proof of a wave equation resolution scheme: the method error**, with Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, and Pierre Weis,

for the 1st ITP symposium (2010, Edinburgh, Scotland). Paper. HAL, DOI, BIB.**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. HAL, DOI, BIB.**Proving bounds on real-valued functions with computations**,

for the 4th IJCAR symposium (2008, Sidney, Australia). Paper and talk. HAL, DOI, BIB.**Floating-point arithmetic in the Coq system**,

for the 8th RNC symposium (2008, Santiago de Compostela, Spain). Paper and talk. HAL, BIB.**Proposing Interval Arithmetic for the C++ Standard**, with Hervé Brönnimann and Sylvain Pion,

for the 12th SCAN symposium (2006, Duisburg, Germany). Talk. BIB.**Proof and certification for an accurate discriminant**, with Sylvie Boldo, Marc Daumas, and William Kahan,

for the 12th SCAN symposium (2006, Duisburg, Germany). Talk. BIB.**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. BIB.**When double rounding is odd**, with Sylvie Boldo,

for the 17th IMACS symposium (2005, Paris, France). Paper and talk. HAL, BIB.**Formal certification of arithmetic filters for geometric predicates**, with Sylvain Pion,

for the 17th IMACS symposium (2005, Paris, France). Paper and talk. HAL, BIB.**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. HAL, DOI, BIB.**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. HAL, BIB.**The Boost interval library**, with Hervé Brönnimann and Sylvain Pion,

for the 5th RNC symposium (2003, Lyon, France). Paper and talk. HAL, BIB.

**Computer arithmetic and formal proofs**,

for the 30th JFLA workshop (2019, Les Rousses, France). Paper (in French) and talk.**Formal verification of a floating-point elementary function**,

for the tutorials of the 22nd ARITH conference (2015, Lyon, France). Talk.**Automating the verification of floating-point algorithms**,

for the 12th SMT workshop (2014, Vienna, Austria). Talk.**Automated methods for verifying floating-point algorithms**,

for MSC (2014, Lyon, France). Talk.**Automations for verifying floating-point algorithms**,

for the 5th Coq workshop (2013, Rennes, France). Talk.**Wave equation numerical resolution: a comprehensive mechanized proof of a C program**,

for the CaCoS workshop (2012, Grenoble, France). Talk.**Numerical computations and formal methods**,

for the 3rd RAIM (2009, Lyon, France). Talk.**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). DOI.

**Directed rounding arithmetic operations**, with Sylvain Pion,

for the C++ standardization committee (2009). Technical report. BIB.**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. BIB.**Bool_set: multi-valued logic**, with Hervé Brönnimann and Sylvain Pion,

for the C++ standardization committee (2006). Technical report. BIB.

- Boost.Interval: a generic interval library for C++.
- Coq : a proof assistant.
- CoqInterval: tactics for proving inequalities on real-valued expressions in Coq.
- Coquelicot: a user-friendly library for real analysis in Coq.
- Flocq: a multi-radix multi-format multi-precision formalization of floating-point arithmetic in Coq.
- Gappa: a tool for formally verifying numerical applications.
- Remake: a tiny clone of make with support for dynamic dependencies.
- Why3: a software verification platform.
- WhyMP: an efficient C library for computing with large integers, verified using Why3.
- Some minor contributions to Why and Frama-C.

- Fresco (ERC 101001995).
- NuSCAP (ANR-20-CE48-0014).
- FastRelax (ANR-14-CE25-0018).
- Soprano (ANR-14-CE28-0020).
- Verasco (ANR-11-INSE-03).
- Coquelicot (Digiteo cluster and Île-de-France regional council).
- FOST (ANR-08-BLAN-0246).

E-mail: | `guillaume.melquiond@inria.fr` |

Address: | LMF - Bâtiment 650 Université Paris-Sud 91405 ORSAY cedex FRANCE |

Phone: | +33 1 69 15 70 98 |

Last update: July 27th, 2023.