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: Proving concurrent noninterference

PorJosé A. Alonso

En la CPP 2012 (The Second International Conference on Certified Programs and Proofs), que comenzará el 13 de diciembre, se presentará un trabajo de verificación formal en Isabelle/HOL titulado Proving concurrent noninterference.

Sus autores son Andrei Popescu, Johannes Hölzl y Tobias Nipkow (del grupo de demostración automática (Theorem Proving Group) de la Universidad de Munich).

Su resumen es

We perform a formal analysis of compositionality techniques for proving possibilistic noninterference for a while language with parallel composition. We develop a uniform framework where we express a wide range of noninterference variants from the literature and compare them w.r.t. their contracts: the strength of the security properties they ensure weighed against the harshness of the syntactic conditions they enforce. This results in a simple implementable algorithm for proving that a program has a specific noninterference property, using only compositionality, which captures uniformly several security type-system results from the literature and suggests a further improved type system. All formalism and theorems have been mechanically verified in Isabelle/HOL.

Este trabajo forma parte del proyecto Security Type Systems and Deduction

El código con las teorías correspondiente se encuentra aquí.

Reseña: Formalizing Frankl’s conjecture: FC-families

PorJosé A. Alonso

En las CICM 2012 (Conferences on Intelligent Computer Mathematics) se ha presentado un trabajo de razonamiento formalizado en Isabelle/HOL titulado Formalizing Frankl’s conjecture: FC-families.

Sus autores son Filip Marić, Miodrag Živković y Bojan Vučković (del grupo ARGO (Automated Reasoning GrOup) de la Universidad de Belgrado).

Su resumen es

The Frankl’s conjecture, formulated in 1979. and still open, states that in every family of sets closed for unions there is an element contained in at least half of the sets. FC-families are families for which it is proved that every union-closed family containing them satisfies the Frankl’s condition (e.g., in every union-closed family that contains a one- element set a, the element a is contained in at least half of the sets, so families of the form a are the simplest FC-families). FC-families play an important role in attacking the Frankl’s conjecture, since they enable significant search space pruning. We present a formalization of the computer assisted approach for proving that a family is an FC-family. Proof-by-computation paradigm is used and the proof assistant Isabelle/HOL is used both to check mathematical content, and to perform (verified) combinatorial searches on which the proofs rely. FC-families known in the literature are confirmed, and a new FC-family is discovered.

El código con la formalización en Isabelle/HOL se encuentra aquí.

Reseña: Interactive and automated proofs for graph transformations

PorJosé A. Alonso

Se ha publicado un trabajo de razonamiento formalizado en Isabelle/HOL titulado Interactive and automated proofs for graph transformations.

Su autor es Martin Strecker (de la Univ. Paul Sabatier, Toulouse, Francia).

Su resumen es

This article explores methods to provide computer support for reasoning about graph transformations. We first define a general framework for representing graphs, graph morphisms and single graph rewriting steps. This setup allows for interactively reasoning about graph transformations. In order to achieve a higher degree of automation, we identify fragments of the graph description language in which we can reduce reasoning about global graph properties to reasoning about local properties, involving only a bounded number of nodes, which can be decided by Boolean satisfiability solving or even by deterministic computation of low complexity.

El código de la formalización se encuentra aquí.