IMDEA Software

IMDEA initiative

Home > Events > Invited Talks > 2018 > Verified Checking of Finite-Precision Error Bounds using Affine Arithmetic

Nikita Zyuzin

Friday, June 29, 2018

10:45am Meeting room 302 (Mountain View), level 3

Nikita Zyuzin, Research Professor, Saarland University, Germany

Verified Checking of Finite-Precision Error Bounds using Affine Arithmetic

Abstract:

Finite-precision representation and approximation of continuous and infinite real numbers causes unavoidable rounding towards discrete and finite values in that precision. Computation with rounded numbers in turn makes the rounding accumulate and further diverge from the exact real-valued computation. Sound and accurate estimation of potential errors caused by this divergence is essential for being able to correctly find an upper bound for the errors of finite-precision computation.

In this talk I will present FloVer, a formally verified certificate checker for automated verification of finite-precision error bounds. I will focus on the ongoing work of formalizing affine arithmetic for FloVer and using it to increase accuracy of the verified roundoff errors. This ongoing work is the subject of my Masters thesis at Saarland University.