Formal verification of tricky numerical computations

Abstract : Computer arithmetic has applied formal methods and formal proofs for years. As the systems may be critical and as the properties may be complex to prove (many sub-cases, error-prone computations), a formal guarantee of correctness is a wish that can now be fulfilled. This talk will present a chain of tools to formally verify numerical programs. The idea is to precisely specify what the program requires and ensures. Then, using deductive verification, the tools produce proof obligation that may be proved either automatically or interac-tively in order to guarantee the correctness of the specifications. Many examples of programs from the literature will be specified and formally verified.
Complete list of metadatas

https://hal.inria.fr/hal-01088692
Contributor : Sylvie Boldo <>
Submitted on : Friday, November 28, 2014 - 2:14:03 PM
Last modification on : Thursday, October 3, 2019 - 2:04:03 PM
Long-term archiving on : Friday, April 14, 2017 - 11:02:28 PM

File

article.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01088692, version 1

Collections

Citation

Sylvie Boldo. Formal verification of tricky numerical computations. 16th GAMM-IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, Sep 2014, Würzburg, Germany. pp.39. ⟨hal-01088692⟩

Share

Metrics

Record views

270

Files downloads

201