Skip to Main content Skip to Navigation
Conference papers

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 metadata
Contributor : Sylvie Boldo Connect in order to contact the contributor
Submitted on : Friday, November 28, 2014 - 2:14:03 PM
Last modification on : Thursday, July 8, 2021 - 3:48:44 AM
Long-term archiving on: : Friday, April 14, 2017 - 11:02:28 PM


Files produced by the author(s)


  • HAL Id : hal-01088692, version 1



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⟩



Les métriques sont temporairement indisponibles