This workshop gathered specialists of computer arithmetic, formal proof systems, computer algebra, rigorous computing and optimal control theory. The aim was to exchange tools and ideas to develop computer-aided proofs of numerical values, with certified and reasonably tight error bounds, without sacrificing efficiency.

This workshop concluded a project funded by the French ANR. It was open to members of that project and to colleagues of various origins sharing our interest in these topics.

The workshop took place in ENS de Lyon, Campus Descartes, Room D2 034.

Invited Speakers

Registration

Registration is free, but necessary (we need it to plan badges, coffee breaks, lunches). Please use the registration form (before April 15.)

Program

Wednesday, May 22

10:00
Welcome
10:30
Lloyd N. Trefethen New Laplace and Helmholtz solvers Slides
11:30
Florent Bréhard A certificate-based approach to formally verified approximations Slides
12:00
Lunch
14:30
Javier Segura Computation of classical orthogonal polynomials and their associated Gauss quadrature rules Slides
15:30
Jean-Michel Muller Error analysis of some operations involved in the Fast Fourier Transform Slides
16:00
Guillaume Melquiond Formal Verification of a State-of-the-Art Integer Square Root Slides
16:30
Break
17:00
Juliette Leblond About some inverse magnetic moment estimation problems and computations of numerical magnetometers Slides
18:00
Nicolas Brisebarre Exponential sums and correctly-rounded functions Slides

Thursday, May 23

10:00
Vincenzo Innocente Small, Fast, Accurate: Arithmetic Challenges in Particle Physics Slides (big file)
11:00
Sylvie Boldo Formal verification about the floating-point average Slides
11:30
Fredrik Johansson Fungrim: the Mathematical Functions Grimoire Slides
12:00
Lunch
14:30
Khalil Ghorbal Formal Verification and Generation of Semi-Algebraic Invariant Sets for Polynomial Autonomous ODEs. Slides
15:30
Marc Mezzarobba Recent improvements to the ore_algebra package Slides
16:00
Laurent Théry Computing Chebyshev models in Coq Slides
16:30
Break
17:00
Bernhard Beckermann Solving singular integral equations with orthogonal rational functions
18:00
Mioara Joldes On moment problems with holonomic functions

Friday, May 24

10:00
Warwick Tucker Small divisors and normal forms Slides
11:00
Florian Steinberg Some formal proofs about evaluation of polynomials over floating-point numbers
11:30
Bruno Salvy Lattice walks and reliable dominant eigenvalues of Laplacians on spherical triangles Slides
12:00
Lunch