The annotated C file and the Coq proofs are available here as .tar.gz.
You may also browse the files:
Numerical program formally proved!
E-mail:Sylvie.Boldo@inria.fr
Address: Sylvie Boldo PCRI - Bat. 650 Université Paris-Sud 91405 ORSAY Cedex FRANCE