Bienvenue
Real2Float is a framework to provide upper bounds of absolute rounding errors. This tool is based on optimization techniques employing semidefinite programming and sparse sums of squares certificates, which can be formally checked inside the Coq theorem prover. The tool can analyze a wide range of nonlinear programs, including polynomials and transcendental operations as well as conditional statements.