|
|
 |
|
Formal Methods Seminar by Sylvie Boldo |
|
Date: March 18, 2005
Time: 10:30am
Location: NIA, Rm 404
Speaker: Sylvie Boldo, ENS Lyon
Subject: "Formal Certification for the Implementation of Elementary Functions"
I will present our latest results with floating-point numbers using the Coq proof assistant. Formal proofs are used to guarantee the accuracy of the floating-point computation of an elementary function (sine, exponential...) After a presentation of floating-point numbers, I will describe the 2 steps of such an evaluation: argument reduction and polynomial evaluation. Our first development guarantees that, under reasonable assumptions, argument reduction provides very precise results when using a fused multiply and accumulate operation only twice. The other development shows that the polynomials used after table look-up provide faithfully rounded results. As our lemmas were checked by a proof assistant, we are pretty sure that no case (as denormal numbers for example) was forgotten and that the final results can be trusted.
|
|
|
Home