NATIONAL INSTITUTE OF AEROSPACE

1.20.17 Titolo/Moscato

1.20.17 Titolo/Moscato

Title: FM Seminar: A Static Analysis Framework for the Estimation of Verified Floating-Point Round-Off Errors

Date: Friday, January 20, 2017

Speakers: Laura Titolo, NIA and Mariano Moscato, NIA

Location: NASA B1220-R110

Time: 10:30AM-11:30AM

Host: Cesar Munzo, NASA/LaRC

Abstract: Round-off errors in floating-point computations can lead to catastrophic consequences when occurring in safety-critical systems. In this talk, a static analysis framework for computing formally verified round-off error bounds of floating-point functional expressions is presented. This framework is based on a denotational semantics that computes a symbolic estimation of floating-point round-off errors along with a proof certificate that ensures its correctness. The symbolic estimation can be evaluated on concrete inputs using rigorous enclosure methods to produce formally verified numerical error bounds. A prototype implementation of the proposed framework is presented, together with some examples of use taken from NASA verification efforts.

BUSINESS WITH NIA

Headquarters

100 Exploration Way
Hampton, VA 23666
(757)325-6700
www.nianet.org