Certifying the Floating-Point Implementation of an Elementary Function Using Gappa
From MaRDI portal
Publication:5280635
DOI10.1109/TC.2010.128zbMath1367.65250MaRDI QIDQ5280635
Guillaume Melquiond, Florent de Dinechin, Ch. Lauter
Publication date: 27 July 2017
Published in: IEEE Transactions on Computers (Search for Journal in Brave)
Related Items (9)
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 ⋮ Trusting computations: a mechanized proof from partial differential equations to actual program ⋮ Floating-point arithmetic ⋮ A two-phase approach for conditional floating-point verification ⋮ Formal analysis of the compact position reporting algorithm ⋮ A formally verified floating-point implementation of the compact position reporting algorithm ⋮ Fast and correctly rounded logarithms in double-precision ⋮ Formalization of Bernstein polynomials and applications to global optimization
Uses Software
This page was built for publication: Certifying the Floating-Point Implementation of an Elementary Function Using Gappa
