Page Tools


Formal Proof, Symbolic Computation and Computer Arithmetic

Slides of the talks

The slides of the talks are available from this page.

Dates and Location

From February 3 to February 7, I.S.F.A. (How to get there.)

The talks will take place in Amphitheater G2 (ground floor) of ISFA.

The welcome and coffee breaks will take place in the main entrance hall (ground floor) of ISFA.

Organizers

Invited Speakers

Presentation

Many critical systems (by « critical » we mean that their failure could have serious consequences) depend largely on software tools that need to be efficient but, above all, are required to be perfectly safe. Examples are the management of nuclear power plants; fully automated public transportation; computer-assisted driving of aircraft, satellites, and helicopters; computer-assisted breaking in automobiles, etc. To fulfill this ultimate safety goal, the use of formal proof is gradually spreading, already with great success in domains such as avionics. However, major difficulties still remain when it comes to formally prove the many critical algorithms and numerical codes that we encounter, such as those that calculate certified approximations to solutions of some differential systems.

Note that even at the lowest level, the validation of some basic arithmetic operations or short sequences of such operations on a processor is still a real challenge in terms of formal proof. We would like that week to be an opportunity to develop and launch new projects around the following closely related issues:

  • Formal proof of elementary operations of floating-point arithmetic,
  • Formal proof of function evaluation processes, of certifications of rational or polynomial approximations to solutions of certain differential equations.

This meeting should gather specialists of numerical computing and formal proof, but also experts in symbolic computation. It is indeed reasonable to expect that the introduction of a significant part of computer algebra in numerical algorithms can foster progress in their formalization and the codes that result.

Talk proposals (Extended deadline !)

Participants are encouraged to submit talk proposals before Dec. 20, 2013 (extended deadline). To do so please send a mail with subject line 'MSC2014:week 4 talk proposal', containing the title and a short text abstract, to the two organizers {nicolas.brisebarre,jean-michel.muller}@ens-lyon.fr. We might have to do some selection depending on the number of proposals.

Schedule

See abstracts below.

Monday 3
9:30 Welcome - coffee - presentation of the conference
10:30 John Harrison 1 An overview of automated reasoning
11:30 Lunch
14:00 Jean-Christophe Filliâtre Deductive Program Verification with Why3
15:00 Assia Mahboubi A computer-aided formal proof of the irrationality of zeta(3)
16:00 Coffee break
16:30 Cyril Cohen CoqEAL - The Coq Effective Algebra Library
Tuesday 4
9:00 Laurent Théry Verifying hardest-to-round computation
10:00 Coffee break
10:30 Sylvie Boldo Formal Verification of Floating-Point Algorithms and Programs
11:30 Lunch
14:00 Free discussion
15:00 John Harrison 2 Applications of automated reasoning
16:00 Coffee break
16:30 Catherine Lelay More than real analysis in Coq
Wednesday 5
9:00 Warwick Tucker 1 Relative equilibria for the n-body problem
10:00 Coffee break
10:30 Micaela MayeroFormal Verification of Scientific Computing Programs
11:30 Lunch
Thursday 6
9:00 Warwick Tucker 2 Fixed points of a destabilized Kuramoto-Sivashinsky equation
10:00 Coffee break
10:30 Guillaume Melquiond Automations for verifying floating-point algorithms
11:30 Lunch
14:00 Free discussion
15:00 Frédéric Chyzak DDMF: A Generated, Online Dictionary of Special Functions
15:45 Coffee break
16:15 Mioara Joldeş Searching for sinks of Henon map using a multiple-precision GPU arithmetic library
20:00 Dinner
Friday 7
9:00 Yves Bertot PI, Arithmetic geometric means, and formal verification in Coq using Coquelicot
10:00 Coffee break
10:30 Marc Mezzarobba Numerical Evaluation of Ai(x) with Reduced Cancellation
11:30 Closing remarks
12:00 Lunch

Abstracts

Yves Bertot (Inria Sophia-Antipolis - Méditerranée, France)
PI, Arithmetic geometric means, and formal verification in Coq using Coquelicot

In an experiment spanning over several months, we formally verified an abstract model of an algorithm to compute PI to a large number of digits using arithmetic geometric means.

The proof that we used relies on a few non elementary aspects, like reasoning about improper integrals or deriving under the integral sign, and revolved around manipulating real numbers. This is why we call this an abstract model.

Then we used the recent extension of Coq with native compilation to test the algorithm on a concrete setting, using large integers. As a result we are able to compute in the order of a million of decimals of PI within the theorem prover. We hope to finish the proofs of the concrete implementation before the workshop.

This work benefits from the overall quality of the Coq system and the following recent contributions: the coquelicot library by Boldo & al., the psatzl tactic by F. Besson, and native compilation by M. Dénès.

Sylvie Boldo (Inria Saclay - Île-de-France, France)
Formal Verification of Floating-Point Algorithms and Programs

Computer arithmetic has applied formal methods and formal proofs for years. As the systems may be critical and as the properties may be complex to prove (many subcases, error-prone computations), a formal guarantee of correctness is a wish that can now be fulfilled.

This lecture will first present the Flocq library, a Coq library that offers a multi-radix and multi-precision formalization for various floating- and fixed-point formats. Examples of proved algorithms from the literature will be given.

The next step is convincing people that what you have formally proved is what you claim/what they need. A way is to display the corresponding proved program. The idea is to precisely specify what the program requires and ensures and to prove the produced proof obligations (see J.-C. Filliâtre's talk). This gives a readable and convincing specification, even if this has drawbacks. As before, examples will be given.

Frédéric Chyzak (Inria Saclay - Île-de-France, France)
DDMF: A Generated, Online Dictionary of Special Functions

Special functions are used in many areas of applied mathematics and the continuous need of scientists for lists of their mathematical properties has led to a great deal of reference books on special functions. Formulas in such books are typically collected from the litterature by mathematical experts. Furthermore, more and more algorithmic properties that have been studied intensively.

Thus, it has become just natural to automate the writing of a mathematical handbook on special functions, insofar as a sufficiently large and well identified class of functions share common algorithmic properties. Our encyclopedia DDMF (for “Dynamic Dictionary of Mathematical Functions”) focuses on so-called “differentiably finite functions”, that is, functions that are described as solutions of a linear differential equation with polynomial coefficients and finitely many initial conditions. These functions enjoy a great deal of common algorithmic properties that have been studied intensively.

For each mathematical function, the current version (v1.9) algorithmically computes, then displays: its potential symmetries; Taylor and Chebyshev series expansions; more generally, asymptotic expansions given in closed form or through definitions by recurrence; calculations of guaranteed, arbitrary-precision numerical approximations; real plots; its Laplace transform; expressions in terms of hypergeometric functions. Upon request by the user, more terms in series expansions or more digits in numerical approximations can be computed incrementally. For some of the properties, human-readable proofs are also automatically generated and displayed. Interestingly enough, the supported functions also include functions with parameters, like Bessel functions and orthogonal polynomials, for which a symbolic treatment of the parameter is performed. In addition, our encyclopedia can in principle be augmented with any new function of the class.

This talk will mostly consist of a demonstration of the mathematical web site (http://ddmf.msr-inria.inria.fr).

Joint work with Alexandre Benoit, Alexis Darrasse, Stefan Gerhold, Christoph Koutschan, Marc Mezzarobba, and Bruno Salvy.

Cyril Cohen (University of Gothenburg, Sweden)
CoqEAL - The Coq Effective Algebra Library

Formal verification of algorithms often requires a choice between definitions that are easy to reason about and definitions that are computationally efficient. One way to reconcile both consists in adopting a high-level view when proving correctness and then refining stepwise down to an efficient low-level implementation. CoqEAL is a library based on refinements for developing formally verified computer algebra algorithms that can be run inside Coq. The methodology allows us to prove the correctness of algorithms on a proof oriented description taking advantage of the Mathematical Components library, and then refine it to an efficient computation-oriented version. The proofs are transported mostly automatically using ideas found in the proof of the parametricity theorem for functional programming languages.

This is a joint work with Anders Mörtberg and Maxime Dénès.

Jean-Christophe Filliâtre (CNRS-LRI, Orsay, France)
Deductive Program Verification with Why3

This talk is an introduction to deductive program verification and to the tool Why3. This tool provides an imperative programming language (with polymorphism, algebraic data types, pattern matching, exceptions, references, arrays, etc.), a mathematical language that is an extension of first-order logic, and a technology to discharge verification conditions using several, off-the-shelf interactive and automated theorem provers (Coq, Alt-Ergo, Z3, CVC3, etc.). Through many examples, this talks intends to show the current state of deductive program verification.

John Harrison (Intel Corporation, USA)
An overview of automated reasoning

The idea of automating logical reasoning is an old dream, going back at least to Leibniz. Since the start of the computer era there has been extensive research in a variety of areas, and I will give a broad overview to establish some perspective, emphasizing both the similarities and differences with computer algebra and how the two fields may be combined.

Applications of automated reasoning

As well as pure intellectual interest, automated reasoning has often been pursued for concrete practical reasons. One is its application to the complete formalization of ordinary mathematical proofs, which might ultimately be hoped to supplement or even replace traditional peer review. Another is to extend mathematical proof to verification of computer sysmtes (programs, hardware, protocols etc.) I will give a survey of some of the major results in this area and remaining challenges.

Mioara Joldeş (CNRS, LAAS, Toulouse, France)
Searching for sinks of Henon map using a multiple-precision GPU arithmetic library

GPUs represent nowadays an important development hardware platform for many scientific computing applications that demand massive parallel computations, but currently GPU-tuned multiple precision arithmetic libraries are scarce. We develop a multiple-precision floating-point arithmetic library using the CUDA programming language for the NVidia GPU platform. In our case, we are currently using this library for locating invariant sets for chaotic dynamical systems. We present a numerical study, GPU implementation and a posteriori validation of existence of stable periodic orbits (sinks) for the Henon map for parameter values close to the canonical ones.

This is a joint work with V. Popescu and W. Tucker.

Catherine Lelay (Inria Saclay - Île-de-France, France)
More than real analysis in Coq

For mathematicians, analysis is not restrained to the set of real numbers R. But few theorem provers have a library of analysis with more than real numbers. And even then, these libraries often duplicate the theorems to deal both with real, complex and multivariate analysis. I will present the Coquelicot library, which aimed to ease proofs of real analysis in Coq. I will also present its recent improvements in order to cover other sets such as complex numbers or matrices without duplication. This was done by the construction of an algebraic hierarchy to express once common properties.

Assia Mahboubi (Inria Saclay - Île-de-France, France)
A computer-aided formal proof of the irrationality of zeta(3)

The study of the evaluations of the Riemann zeta function at positive odd integers remains as of today an active topic of research in number theory. R. Apéry obtained a spectacular success in 1978 when he established the irrationality of zeta(3). However the (ir)rationality status of the other positive integer values in still unknown. The crux of Apéry's original presentation of this result is to observe that certain two sequences satisfy a common recurrence which allows for a precise estimation of their respective asymptotic behaviour. However, both guessing and verifying this recurrence was a difficult problem at the time. Since the 90's, combinatorialists and computer-algebraists have devised algorithms that are able to output such recurrences, leading to so-called “computer-algebra proofs”. In this talk we describe a formal proof of the irrationality of zeta(3) based on a computer algebra session running these algorithms and we discuss the issues and perspectives raised by such a collaboration of a computer algebra system and a proof assistant.

This is a joint work with Frédéric Chyzak (Inria), Thomas Sibut-Pinote (ENS de Lyon) and Enrico Tassi (Inria).

Micaela Mayero (Université Paris Nord, France)
Formal Verification of Scientific Computing Programs

Several reasons can make programs fail: out-of-bound array accesses, simply coding errors or floating-point computations that lead to round-off errors. Scientific computing programs, that may be critical, make no exception in that respect. We present methods and tools for proving the correct behavior of programs and we have extended them for the verification of an existing numerical analysis program. This C program implements the second-order centered finite difference explicit scheme for solving the 1D wave equation.

This is a joint work with Sylvie Boldo (Inria), François Clément (Inria), Jean-Christophe Filliâtre (CNRS), Guillaume Melquiond (Inria) and Pierre Weis (Inria).

Guillaume Melquiond (Inria Saclay - Île-de-France, France)
Automations for verifying floating-point algorithms

Floating-point numbers are limited both in range and in precision, yet they are widely used as a way to implement computations on real numbers. Thus arithmetic operations cause small errors that might be amplified during subsequent computations. As such, it is important to guarantee that the computed values are still close enough to the ideal results. The traditional way to tackle the verification of such programs is to perform an error analysis, possibly using automated tools.

Unfortunately, when it comes to the low-level floating-point functions found in mathematical libraries, the code is usually so contrived that this approach falls short. Falling back to a pen-and-paper proof makes it possible to verify such functions, but this process is long, tedious, and error-prone. Formal proofs take care of that last point, but they come at an even greater cost for the user. Thus one needs to recover some automations inside proof assistants to ease the verification process.

This lecture will present the Gappa tool and how it integrates with the Coq proof assistant. The presentation will give an overview of the inner workings of the tool and then focus on showing how it can be used in practice to verify floating-point algorithms.

Marc Mezzarobba (CNRS, LIP6, Paris, France)
Numerical Evaluation of Ai(x) with Reduced Cancellation

The series expansion at the origin of the Airy function Ai(x) converges on the whole complex plane. Its coefficients are given by a simple recursion. However, the series is alternating, and for moderately large x > 0, its sum is difficult to compute in finite-precision arithmetic due to a phenomenon known as catastrophic cancellation. After presenting this phenomenon, I will explain how to find two auxiliary series F and G, both with nonnegative coefficients, such that Ai(x) = G(x)/F(x). This step is based on a variant of a method due by Gawronski, Müller, and Reinhard. Both auxiliary sums are well-conditioned, but the Taylor coefficients of G turn out to obey an ill-conditioned recurrence relation. We will use the classical Miller backward recurrence method to overcome this issue. Finally, I will outline the error analysis of the resulting algorithm, in which so-called saddle-point estimates on the coefficients of G are used to obtain rigorous bounds for both the method error and the round-off errors.

This is joint work with Sylvain Chevillard (APICS, Inria).

Laurent Théry (Inria Sophia-Antipolis - Méditerranée, France)
Verifying hardest-to-round computation

In order to derive an efficient and robust floating-point implementation for a function f in a floating-point format F, it is crucial to compute its hardest-to-round points, i.e. the floating point numbers x such that f(x) is closest to the midpoint of two consecutive floating point numbers in the format F. In this talk, we will show how formal verification can be applied to this kind of computations.

Warwick Tucker (Uppsala University, Sweden)
Relative equilibria for the n-body problem

An old problem, raised by Wintner in 1941, is to find the number of special configurations, known as relative equilibria, in the classical n-body problem from celestial mechanics. A relative equilibrium is a special – planar – configuration of masses of the n-body problem, which rotates rigidly about its center of mass, given the correct initial momenta. Unlike most previous attempts at solving this problem, where large systems of polynomial equations are analysed, our approach will rely upon techniques from analysis, rather than from algebraic geometry. We will use a set of tools and techniques based on set-valued analysis and computer-assisted proofs. This provides a means for solving general nonlinear systems of equations, and will thus extend to non-Newtonian settings too. A challenging part of this problem is to understand how the number of solutions of a finitely parametrized system of equations changes as the parameters (the masses of the bodies in our case) are varied. When such a bifurcation takes place, the analysis of the system must be constrained to a special submanifold, and carefully examined there. By computing Taylor expansions (with rigorous error bounds) of the governing equations on these manifolds, we can account for the bifurcations taking place. This is ongoing work.

Fixed points of a destabilized Kuramoto-Sivashinsky equation

We consider the family of destabilized Kuramoto-Sivashinsky equations in one spatial dimension ut + ν uxxxx + β uxx + γ u ux = α u for α, ν ≥ 0 and β, γ ∈ R. For certain parameter values, shock-like stationary solutions have been numerically observed. We verify the existence of several such solutions using the framework of self-consistent bounds and validated numerics. This is joint work with Ferenc A. Bartha.