scientific article; zbMATH DE number 1863384
From MaRDI portal
Publication:4790659
zbMath1005.68544MaRDI QIDQ4790659
Laurent Théry, Laurence Rideau, Marc Daumas
Publication date: 4 February 2003
Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2152/21520169
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items (18)
Semantics of roundoff error propagation in finite precision calculations ⋮ Formalization of Double-Word Arithmetic, and Comments on “Tight and Rigorous Error Bounds for Basic Building Blocks of Double-Word Arithmetic” ⋮ Computing predecessor and successor in rounding to nearest ⋮ 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 ⋮ Finding normal binary floating-point factors efficiently ⋮ Formal verification of numerical programs: from C annotated programs to mechanical proofs ⋮ A validated real function calculus ⋮ Proving Bounds on Real-Valued Functions with Computations ⋮ Deciding floating-point logic with abstract conflict driven clause learning ⋮ Multi-Prover Verification of Floating-Point Programs ⋮ Floating-point arithmetic in the Coq system ⋮ A parameterized floating-point formalizaton in HOL Light ⋮ Combining Coq and Gappa for Certifying Floating-Point Programs ⋮ Additive symmetries: The non-negative case. ⋮ Formal verification of the VAMP floating point unit ⋮ Formalization of fixed-point arithmetic in HOL
Uses Software
This page was built for publication:
