A Formally-Verified C Compiler Supporting Floating-Point Arithmetic
IEEE Symposium on Computer Arithmetic, pp. 107-115, 2013.
floating-point arithmeticsource languageieee-754 standardfinal resultfloating-point programMore(14+)
Floating-point arithmetic is known to be tricky: roundings, formats, exceptional values. The IEEE-754 standard was a push towards straightening the field and made formal reasoning about floating-point computations easier and flourishing. Unfortunately, this is not sufficient to guarantee the final result of a program, as several other act...More
Full Text (Upload PDF)
PPT (Upload PPT)