Reseña: Proofs of properties of finite-dimensional vector spaces using Isabelle/HOL

PorJosé A. Alonso

Se ha publicado un trabajo de razonamiento formalizado en Isabelle/HOL, titulada Proofs of properties of finite-dimensional vector spaces using Isabelle/HOL.

Su autor es Jose Divasón Mallagaray, dirigido por Jesús María Aransay Azofra (de la Univ. de la Rioja).

La presentación del trabajo tuvo lugar el 25 de Octubre de 2011 en la Universidad de la Rioja.

El objetivo del trabajo es la formalización en Isabelle/HOL de conceptos y teoremas sobre álgebra lineal siguiendo la 16 primeras secciones del libro de Halmos Finite-dimensional vector spaces.

El resumen del trabajo es

In this work we deal with finite-dimensional vector spaces over a generic field \mathbb{K}. First we will state properties of vector spaces independently of their dimension. Then, we will introduce the conditions to obtain finite-dimensional vector spaces. The notions of linear dependence and independence, as well as linear combinations, and hence the notion of basis will be presented. Some results about the dimension of the different basis of a vector space will be necessary, as well as on the isomorphism among vector spaces. Once we have introduced the notion of basis, and with the additional condition of it being finite, we will introduce the notion of finite-dimensional vector space. Next step is to introduce vector subspaces. We will pay attention to vector susbpaces generated by a given set of vectors and prove some of their properties. The notion of linear maps will be also required to define isomorphisms of vector spaces. Finally, we will prove that a vector space (over a field \mathbb{K}) of (finite) dimension n is isomorphic to \mathbb{K}^n.

The previous results will be presented following the book by Halmos on vector spaces [1]. Its formalization will be carried out in Isabelle/HOL.

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

Una extensión del trabajo es Formalizing an abstract algebra textbook in Isabelle/HOL presentado el 14 de junio de 2012 en el EACA 2012 (EACA 2012
XIII Encuentro de Álgebra Computacional y Aplicaciones).

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

Reseña: Towards provably robust watermarking

PorJosé A. Alonso

El martes (14 de agosto de 2012) se presentó en el ITP 2012 (Interactive Theorem Proving) un trabajo de razonamiento formalizado en Coq titulado Towards provably robust watermarking.

Sus autores son David Baelde, Pierre Courtieu, David Gross-Amblard y
Christine Paulin-Mohring.

El resumen del trabajo es

Watermarking techniques are used to help identifying copies of publicly released information. They consist in applying a slight and secret modification to the data before its release, in a way that should be robust, ie., remain recognizable even in (reasonably) modified copies of the data. In this paper, we present new results about the robustness of watermarking schemes against arbitrary attackers, and the formalization of those results in Coq. We used the ALEA library, which formalizes probability theory and models probabilistic programs using a simple monadic translation. This work illustrates the strengths and particularities of the induced style of reasoning about probabilistic programs. Our technique for proving robustness is adapted from methods commonly used for cryptographic protocols, and we discuss its relevance to the field of watermarking.

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

El trabajo es parte del proyecto SCALP (Security of Cryptographic ALgorithms with Probabilities).

Reseña: Correctness of pointer manipulating algorithms illustrated by a verified BDD construction

PorJosé A. Alonso

Se ha publicado un nuevo trabajo de verificación formal en Isabelle/HOL titulado Correctness of pointer manipulating algorithms illustrated by a verified BDD construction.

Los autores del trabajo son Mathieu Giorgino y Martin Strecker (de la Univ. de Toulouse).

El trabajo se presentará el 29 de agosto en el FM 2012 (18th International Symposium on Formal Methods).

En el trabajo se presenta una metodología para la verificación de programas imperativos usando el asistente de prueba Isabelle/HOL y su extensión Imperative_HOL, junto con el generador de código Scala de Isabelle. Como aplicación de la metodología se verifica los diagramas de decisión binarios (BDD).

Su resumen es

This paper is an extended case study using a high-level approach to the verification of graph transformation algorithms: To represent sharing, graphs are considered as trees with additional pointers, and algorithms manipulating them are essentially primitive recursive traversals written in a monadic style. With this, we achieve almost trivial termination arguments and can use inductive reasoning principles for showing the correctness of the algorithms. We illustrate the approach with the verification of a BDD package which is modular in that it can be instantiated with different implementations of association tables for node lookup. We have also implemented a garbage collector for freeing association tables from unused entries. Even without low-level optimizations, the resulting implementation is reasonably efficient.

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

El trabajo es parte del proyecto CLIMT (Categorical and Logical Methods in Model Transformation).

Reseña: Construction of real algebraic numbers in Coq

PorJosé A. Alonso

El lunes (13 de agosto de 2012) se presentó en el ITP 2012 (Interactive Theorem Proving) un trabajo de razonamiento formalizado en Coq titulado Construction of real algebraic numbers in Coq.

Su autor es Cyril Cohen (de la École Polytechnique (Palaiseau, Francia)).

El resumen del trabajo es

This paper shows a construction in Coq of the set of real algebraic numbers, together with a formal proof that this set has a structure of discrete archimedian real closed field. This construction hence implements an interface of real closed field. Instances of such an interface immediately enjoy quantifier elimination thanks to a previous work. This work also intends to be a basis for the construction of complex algebraic numbers and to be a reference implementation for the certification of numerous algorithms relying on algebraic numbers in computer algebra.

El código de la formalización en Coq se encuentra en realalg.tgz.

Reseña: Abstract interpretation of annotated commands

PorJosé A. Alonso

El lunes (13 de agosto de 2012) se presentó en el ITP 2012 (Interactive Theorem Proving) un trabajo de razonamiento formalizado en Isabelle titulado Abstract interpretation of annotated commands.

Su autor es Tobias Nipkow (del Theorem Proving Group de la Technische Universität München).

El resumen del trabajo es

This paper formalises a generic abstract interpreter for a while-language, including widening and narrowing. The collecting semantics and the abstract interpreter operate on annotated commands: the program is represented as a syntax tree with the semantic information directly embedded, without auxiliary labels. The aim of the paper is simplicity of the formalisation, not efficiency or precision. This is motivated by the inclusion of the material in a theorem prover based course on semantics.

Las correspondientes teorías de Isabelle se encuentran aquí.