Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Guillaume Melquiond's page
I am an Inria researcher
in the Toccata /
VALS team from the
LRI (Université Paris Sud).
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
Coq.Interval 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. Coq.Interval
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 aims 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.
Arithmétique des ordinateurs et preuves formelles,
with Sylvie Boldo,
in Informatique Mathématique : une photographie en 2013.
Handbook of Floating-Point Arithmetic, coordinated by
Jean-Michel Muller,
published by Birkhäuser (2010).
Summary.
DOI.
Arithmétique d'intervalles et certification de programmes. Thesis (in French) and
defense.
Journals:
Proving tight bounds on univariate expressions with elementary functions in Coq,
with Érik Martin-Dorel,
in Journal of Automated Reasoning (2015).
Paper.
DOI.
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.
DOI.
Formalization of real analysis: A survey of proof assistants and libraries,
with Sylvie Boldo
and Catherine Lelay,
in Mathematical Structures in Computer Science (2014).
Paper.
DOI.
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.
DOI.
Floating-point arithmetic in the Coq system,
in Information and Computation (2012, volume 216).
Paper.
DOI.
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.
DOI.
Certification of bounds on expressions involving rounded operators,
with Marc Daumas,
in Transactions on Mathematical Software (2010, volume 37.1).
Paper.
DOI.
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.
DOI.
Formally certified floating-point filters for homogeneous geometric predicate,
with Sylvain Pion,
in Theoretical Informatics and Applications (2007, volume 41.1).
Paper.
DOI.
The design of the Boost interval arithmetic library,
with Hervé Brönnimann
and Sylvain Pion,
in Theoretical Computer Science (2006, volume 351).
Paper.
DOI.
Conferences:
Inductive verification of hybrid automata with strongest postcondition calculus,
with Daisuke Ishii
and Shin Nakajima,
for the 10th iFM symposium (2013, Turku, Finland).
Paper.
DOI.
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.
DOI.
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.
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.
DOI.
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.
DOI.
Proving bounds on real-valued functions with computations,
for the 4th IJCAR symposium (2008, Sidney, Australia).
Paper and
talk.
DOI.
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,
Marc Daumas,
and William Kahan,
for the 12th SCAN symposium (2006, Duisburg, Germany).
Talk.
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.
DOI.
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.
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:
Directed rounding arithmetic operations,
with Sylvain Pion,
for the C++ standardization committee (2009).
Technical report.