Proof of properties in floating-point arithmetic

5th November 2015


Speaker: Jean-Michel Muller , directeur de recherche at Ecole Normale SupĂ©rieure, Lyon, France

Abstract: Floating-point (FP) arithmetic was originally designed as a mere approximation to real arithmetic. And yet, since the behaviour of each operation is fully specified by the IEEE-754 standard for floating-point arithmetic, FP arithmetic can also be viewed as a kind of mathematical structure on which it is possible to design algorithms and proofs.