Version française
Guillaume Melquiond
I am an Inria researcher
in the Toccata team
from the LMF laboratory
(Université Paris Saclay).
Research interests
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.
Publications (bibtex)
Books, book chapters, and theses:
- 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.
Journals:
- 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.
Conferences:
- Turning the Coq proof assistant into a pocket calculator,
for the 15th Coq workshop (2024, Tbilisi, Georgia).
HAL,
BIB.
- End-to-end formal verification of a fast and accurate floating-point approximation,
with Florian Faissole
and Paul Geneau de Lamarlière,
for the 15th ITP conference (2024, Tbilisi, Georgia).
HAL,
DOI,
BIB.
- A safe low-level language for computer algebra and its formally verified compiler,
with Josué Moreau,
for the 29th ICFP conference (2024, Milan, Italy).
HAL,
DOI,
BIB.
- Slimmer formal proofs for mathematical libraries,
with Paul Geneau de Lamarlière
and Florian Faissole,
for the 30th ARITH symposium (2023, Portland, OR, USA).
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.
Invited talks:
- 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.
Some reports:
Software development
- 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.
Projects and grants
Contact information
| 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 |
Other resources
Last update: July 27th, 2023.
