Floats and Ropes: A Case Study for Formal Numerical Program Verification
From MaRDI portal
Publication:3638088
DOI10.1007/978-3-642-02930-1_8zbMath1248.65045OpenAlexW1500006811MaRDI QIDQ3638088
Publication date: 14 July 2009
Published in: Automata, Languages and Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-02930-1_8
Specification and verification (program logics, model checking, etc.) (68Q60) Algorithms with automatic result verification (65G20)
Related Items (7)
Wave equation numerical resolution: a comprehensive mechanized proof of a C program ⋮ Trusting computations: a mechanized proof from partial differential equations to actual program ⋮ Formally-verified round-off error analysis of Runge-Kutta methods ⋮ Rounding error analysis of linear recurrences using generating series ⋮ Formal verification of numerical programs: from C annotated programs to mechanical proofs ⋮ Polynomial function intervals for floating-point software verification ⋮ Combining Coq and Gappa for Certifying Floating-Point Programs
Uses Software
This page was built for publication: Floats and Ropes: A Case Study for Formal Numerical Program Verification
