Verified Compilation of Floating-Point Computations

Sylvie Boldo 1, 2 Jacques-Henri Jourdan 3 Xavier Leroy 3 Guillaume Melquiond 2, 1
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
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.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2015, 54 (2), pp.135-163. <10.1007/s10817-014-9317-x>
Liste complète des métadonnées
Contributeur : Sylvie Boldo <>
Soumis le : vendredi 7 novembre 2014 - 16:17:14
Dernière modification le : vendredi 17 février 2017 - 16:10:21
Document(s) archivé(s) le : vendredi 14 avril 2017 - 14:24:34


Fichiers produits par l'(les) auteur(s)



Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond. Verified Compilation of Floating-Point Computations. Journal of Automated Reasoning, Springer Verlag, 2015, 54 (2), pp.135-163. <10.1007/s10817-014-9317-x>. <hal-00862689v3>



Consultations de
la notice


Téléchargements du document