Verified Compilation of Floating-Point Computations

J. Autom. Reasoning, pp. 135-163, 2015.

Cited by: 40|Bibtex|Views14|Links
EI
Keywords:
Floating-point arithmeticCompiler verificationSemantic preservationCompCertCoq

Abstract:

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

Code:

Data:

Your rating :
0

 

Tags
Comments