Sylvie Boldo

Formal verification of tricky numerical computations

Sylvie Boldo
Inria, France

Computer arithmetic has applied formal methods and formal proofs foryears. As the systems may be critical and as the properties may becomplex to prove (many sub-cases, error-prone computations), a formalguarantee of correctness is a wish that can now be fulfilled.

This talk will present a chain of tools to formally verify numericalprograms. The idea is to precisely specify what the program requiresand ensures. Then, using deductive verification, the tools produceproof obligation that may be proved either automatically orinteractively in order to guarantee the correctness of thespecifications. Many examples of programs from the literature will bespecified and formally verified.