Provably faithful evaluation of polynomials

10 years 23 days ago
Provably faithful evaluation of polynomials
We provide sufficient conditions that formally guarantee that the floating-point computation of a polynomial evaluation is faithful. To this end, we develop a formalization of floatingpoint numbers and rounding modes in the Program Verification System (PVS). Our work is based on a well-known formalization of floating-point arithmetic in the proof assistant Coq, where polynomial evaluation has been already studied. However, thanks to the powerful proof automation provided by PVS, the sufficient conditions proposed in our work are more general than the original ones. Categories and Subject Descriptors B.2.3 [Hardware]: Arithmetic and Logic Structures—Reliability, Testing, and Fault-Tolerance; F.4 [Theory of Computation]: Mathematical Logic and Formal Languages Keywords Floating-point, polynomial evaluation, formal verification
Sylvie Boldo, César Muñoz
Added 14 Jun 2010
Updated 14 Jun 2010
Type Conference
Year 2006
Where SAC
Authors Sylvie Boldo, César Muñoz
Comments (0)