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

PorJosé A. Alonso

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í.

Reseña: A string of pearls: Proofs of Fermat’s little theorem

PorJosé A. Alonso

En la CPP12 (The Second International Conference on Certified Programs and Proofs), que comienza el 13 de diciembre, se presentará un trabajo de razonamiento formalizado en HOL4 titulado A string of pearls: Proofs of Fermat’s little theorem.

Sus autores son Hing-Lun Chan (de la Australian National University) y Michael Norrish (del Canberra Research Lab., NICTA).

Su resumen es

We discuss mechanised proofs of Fermat’s Little Theorem in a variety of styles, focusing in particular on an elegant combinatorial “necklace” proof that has not been mechanised previously. What is elegant in prose turns out to be long-winded mechanically, and so we examine the effect of explicitly appealing to group theory. This has pleasant consequences both for the necklace proof, and also for the direct number-theoretic approach.

El código conteniendo las demostraciones en HOL4 se encuentra aquí.

Reseña: Proof pearl – A mechanized proof of GHC’s mergesort

PorJosé A. Alonso

Se publicado un artículo de verificación en Iabelle/HOL titulado Proof pearl – A mechanized proof of GHC’s mergesort.

Su autor es Christian Sternagel (de la Univ. de la Univ. de Insbruck).

Su resumen es

We present our Isabelle/HOL formalization of GHC’s sorting algorithm for lists, proving its correctness and stability. This constitutes another example of applying a state-of-the-art poof assistant to real-world code. Furthermore, it allows users to take advantage of the formalized algorithm in generated code.

La librería estándard de GHC (The Glasgow Haskell Compiler) tiene un algoritmo de ordenación, que es una variante de la ordenación por mezcla. El objetivo del trabajo es la verificación de dicho algortimo en Isabelle/HOL, demostrando su corrección y estabilidad.

La principal característica de este trabajo es la verificación de programas eficientes. El método empleado tiene tres pasos:

  1. formalizar variantes del algoritmo que faciliten la demostración y probar todas las propiedades deseadas;
  2. formalizar variantes eficientes del algoritmo y probar su equivalencia y
  3. usar la generación de código y obtener un programa eficiente del que se tiene garantía que satisface todas las propiedades que se probaron en la formalización inicial.

La formalización es pequeña (menos de 400 líneas de código) y la mayoría de las demostraciones son automáticas. Este éxito se basa en dos principios: la generalización de los conceptos y la definición de esquemas de inducción.

El código en Isabelle/HOL de la teoría correspondiente al trabajo se encuentra en The Archive of Formal Proofs.

Confluence by decreasing diagrams – Formalized

PorJosé A. Alonso

Se ha publicado un trabajo de formalización de sistemas de reescritura en Isabelle/HOL titulado Confluence by decreasing diagrams – formalized.

Su autor es Harald Zankl (de la Universidad de Insbruck, Austria).

Su resumen es

Decreasing diagrams are a complete characterization of confluence for abstract rewrite systems whose convertibility classes are countable. In this paper we present a formalization of decreasing diagrams in the theorem prover Isabelle. The main contribution is a formal proof that any locally decreasing abstract rewrite system is confluent.

Las teorías Isabelle/HOL correspondiente al trabajo se encuentran aquí.

Reseña: A formal proof of Sasaki-Murao algorithm

PorJosé A. Alonso

La semana pasada se presentó en el MAP2012 (Mathematics, Algorithms and Proofs 2012) un trabajo de aplicación de bibliotecas de razonamiento formalizado en Coq a la verificación de un algoritmo de álgebra computacional.

El título del trabajo es A formal proof of Sasaki-Murao algorithm y sus autores son Tierry Coquand, Anders Mörtberg y Vincent Siles (de la Univ. de Gotemburgo, Suecia).

El resumen del trabajo es

The Sasaki-Murao algorithm computes the determinant of any square matrix over a commutative ring in polynomial time. The algorithm itself can be written as a short and simple functional program, but its correctness involves non-trivial mathematics. We here represent this algorithm in Type Theory with a new correctness proof, using the Coq proof assistant and the SSReflect extension.

El código Coq de la formalización se encuentra aquí y las transparencias de la presentación se encuentran aquí.

Este trabajo es parte del proyecto ForMath: Formalisation of Mathematics.