## Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond.
Verified compilation of floating-point computations.
*Journal of Automated Reasoning*, 54(2):135-163, 2015.

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 actors are involved: programming language, compiler, and
architecture. The CompCert formally-verified compiler provides a
solution to this problem: this compiler comes with a mathematical
specification of the semantics of its source language (a large subset
of ISO C99) and target platforms (ARM, PowerPC, x86-SSE2), and with a
proof that compilation preserves semantics. In this paper, we report
on our recent success in formally specifying and proving correct
CompCert's compilation of floating-point arithmetic. Since CompCert
is verified using the Coq proof assistant, this effort required a
suitable Coq formalization of the IEEE-754 standard; we extended the
Flocq library for this purpose. As a result, we obtain the first
formally verified compiler that provably preserves the semantics of
floating-point programs.

[ bib |
Local copy |
At publisher's ]
Back

*This file was generated by
bibtex2html 1.97.*