A Formally-Verified C Compiler Supporting Floating-Point Arithmetic

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 actors are involved: programming language, compiler, 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 C90) 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.
Complete list of metadatas

Cited literature [29 references]  Display  Hide  Download

https://hal.inria.fr/hal-00743090
Contributor : Guillaume Melquiond <>
Submitted on : Friday, January 25, 2013 - 7:13:15 AM
Last modification on : Thursday, October 3, 2019 - 2:04:03 PM
Long-term archiving on : Friday, April 26, 2013 - 3:54:57 AM

File

article.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00743090, version 2

Collections

Citation

Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond. A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. Arith - 21st IEEE Symposium on Computer Arithmetic, Apr 2013, Austin, United States. pp.107-115. ⟨hal-00743090v2⟩

Share

Metrics

Record views

1880

Files downloads

945