Metalibm

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 is developped by Arénaire and written by 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: 01/07/2010