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

Speaker: Mariano Moscato - National Institute of Aerospace

Data: 03 de Outubro de 2017

Horário: 16h

Local: Auditório do CIC

Abstract: This talk is aimed to present a static analysis technique for computing formally verified round-off error bounds of floating-point functional expressions. The technique 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. The proposed technique is implemented in the prototype research tool PRECiSA (Program Round-off Error Certifier via Static Analysis) and used in the verification of floating-point programs of interest to NASA.