Verified Compilation of Floating-Point Computations
J. Autom. Reasoning, pp. 135-163, 2015.
Floating-point arithmeticCompiler verificationSemantic preservationCompCertCoq
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)