Certifying the Floating-Point Implementation of an Elementary Function Using Gappa

DOI10.1109/TC.2010.128MaRDI QIDQ5280635zbMATH OpenFDO

Authors Florent de Dinechin, Christoph Lauter, Guillaume Melquiond

Publication date 27 July 2017

Published in IEEE Transactions on Computers (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1109/TC.2010.128

Mathematics Subject Classification ID

Numerical algorithms for computer arithmetic, etc. (65Y04)

Cited in

(13)

• Formal analysis of the compact position reporting algorithm
• A formally verified floating-point implementation of the compact position reporting algorithm
• A two-phase approach for conditional floating-point verification
• Formalization of Bernstein polynomials and applications to global optimization
• Trusting computations: a mechanized proof from partial differential equations to actual program
• Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• Fast and correctly rounded logarithms in double-precision
• Floating-point arithmetic
• Provably correct floating-point implementation of a point-in-polygon algorithm
• Algorithm 1029: encapsulated error, a direct approach to evaluate floating-point accuracy
• Formally verified roundoff error bounds on LogSumExp-based computations
• Taming floating-point rounding errors with proofs (invited talk)

Describes a project that uses

Uses Software

• Gappa

This page was built for publication: Certifying the Floating-Point Implementation of an Elementary Function Using Gappa

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5280635)