\( \def\sc#1{\dosc#1\csod} \def\dosc#1#2\csod{{\rm #1{\small #2}}} \def\nlcertify{\textrm{NLCertify}} \def\realtofloat{\textrm{Real2Float}} \def\xb{\mathbf{x}} \def\ocaml{\sc{OCaml}} \def\coq{\sc{Coq}} \def\ssreflect{\sc{Ssreflect}} \def\mathcomp{\sc{MathComp}} \def\hol{\sc{HOL-Light}} \def\sdpa{\sc{Sdpa}} \newcommand{\sollya}{\mathtt{Sollya}} \def\opam{\sc{Opam}} \)


$\realtofloat$ 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.

Install it or have a look at the examples.