Reseña: A formally-verified C compiler supporting floating-point arithmetic

Uno de los principales problemas en la verificación de programas consiste en verificación de propiedades de programas con aritmética flotante. Un avance en dicho problema es el reciente trabajo A formally-verified C compiler supporting floating-point arithmetic.

Sus autores son Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy y Guillaume Melquiond.

Su resumen es

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 possible. 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 (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.

El trabajo está integrado en la versión 1.12 de CompCert que se encuentra aquí.