The **Metalibm** project provides a tool for the
automatic implementation of mathematical (`libm`

)
functions. A function `f` is automatically
transformed
into Gappa-certified `C`

code
implementing an approximation polynomial in a given domain with given
accuracy.

Metalibm is based on the Sollya tool.

**Metalibm** used to be developped
by ArĂ©naire is now developped by PEQUAN and
written
by Olga Kupriianova and
Christoph Lauter using code contributed by
Serge Torres and
Nathalie Revol.

**Metalibm provides you:**

- an automatic tool transforming a function description into floating-point code,
- the automatic generation of a Gappa proof that the produced code is correct,
- an easy way to get approximation polynomials with optimized floating-point coefficients,
- fully automatic handling of code in double, double-double and triple-double precision
- and much more.

**Partnerships:**

- Metalibm is used for generating parts of the CR-Libm library of correctly rounded mathematical functions.
- Metalibm strives to similar goals for software implementations that FloPoCo strives to for hardware.
- Metalibm implements parts of the goals intended by the EVA-Flo project.

**Download Metalibm:**

- No version has been released, yet.
- However, the latest development version is available through anonymous CVS checkout as indicated here.

**Metalibm** is based on the following softwares and software libraries:

- the Sollya tool,
- the Gappa proof tool,
- a C compiler such as gcc and
- a C++ compiler such as g++.

**License:** Metalibm is free software; you can
redistribute it and/or modify it under the terms of the GNU Lesser
General Public License as published by the Free Software Foundation;
either version 2 of the License, or (at your option) any later
version. This program is distributed in the hope that it will be
useful, but WITHOUT ANY WARRANTY; without even the implied warranty
of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
General Public License for more details.

Last update: 05/31/2013