La Lógica en las ciencias computacionales

PorJosé A. Alonso

Se ha publicado un artículo sobre la enseñanza de la lógica titulado La Lógica en las ciencias computacionales.

Su autor es Edgar Serna M. (del Instituto Tecnológico Metropolitano, Medellín (Colombia)).

Su resumen es

En este trabajo se hace un análisis a la necesidad de incluir a la lógica en los procesos formativos en Ciencias Computacionales (CS por sus siglas en inglés). Se parte de un recorrido sobre la historia de la lógica en estas ciencias, posteriormente se describe la relación y la necesidad de incluirla en los procesos formativos relacionados, y al final se analiza qué, cuándo y qué tan profundo se debería trabajar en la formación en CS. Se trata de una revisión al estado del tema y a la importancia de incluirlo en los pregrados y en los posgrados en áreas de ciencias computacionales y tecnologías de información.

El artículo se ha publicado en la Revista Educación en Ingeniería.

Proof pearl: A verified bignum implementation in x86-64 machine code

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal en HOL4 titulado Proof pearl: A verified bignum implementation in x86-64 machine code.

Sus autores son

  • Magnus O. Myreen (de la Universidad de Cambridge)y
  • Gregorio Curello (de la Universidad Autónoma de Barcelona).

Su resumen es

Verification of machine code can easily deteriorate into an endless clutter of low-level details. This paper presents a case study which shows that machine-code verification does not necessarily require ghastly low-level proofs. The case study we describe is the construction of an x86-64 implementation of arbitrary-precision integer arithmetic. Compared with closely related work, our proofs are shorter and, more importantly, the reasoning is at a more convenient high level of abstraction, e.g. pointer reasoning is largely avoided. We achieve this improvement as a result of using previously developed tools, namely, a proof-producing decompiler and compiler. The work presented in this paper has been developed in the HOL4 theorem prover and the case study resulted in 700 lines of verified 64-bit x86 machine code.

El código correspondiente se encuentra aquí.

El trabajo se presentará en la CPP 2013 (3rd International Conference on Certified Programs and Proofs).

Mechanized metatheory for a λ λ-calculus with trust types

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Mechanized metatheory for a λ λ-calculus with trust types.

Sus autores son

Su resumen es

As computer programs become increasingly complex, techniques for ensuring trustworthiness of information manipulated by them become critical. In this work, we use the Coq proof assistant to formalise a λ λ -calculus with trust types, originally formulated by Ørbæk and Palsberg. We give formal proofs of type soundness, erasure and simulation theorems and also prove decidability of the typing problem. As a result of our formalisation a certified type checker is derived.

El código de las correspondientes teorías en Coq se encuentra aquí.

La versión final del trabajo se ha publicado en el Journal of the Brazilian Computer Society.

Proving soundness of combinatorial Vickrey auctions and generating verified executable code

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Proving soundness of combinatorial Vickrey auctions and generating verified executable code.

Sus autores son

Su resumen es

Using mechanised reasoning we prove that combinatorial Vickrey auctions are soundly specified in that they associate a unique outcome (allocation and transfers) to any valid input (bids). Having done so, we auto-generate verified executable code from the formally defined auction. This removes a source of error in implementing the auction design. We intend to use formal methods to verify new auction designs. Here, our contribution is to introduce and demonstrate the use of formal methods for auction verification in the familiar setting of a well-known auction.

El trabajo se ha desarrollado como parte del proyecto ForMaRE (Formal Mathematical Reasoning in Economics).

El código de las correspondientes teorías en Isabelle se encuentra aquí.

A computer-assisted proof of correctness of a marching cubes algorithm

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq titulado A computer-assisted proof of correctness of a marching cubes algorithm.

Sus autores son Andrey N. Chernikov y Jing Xu (de la Old Dominion University, Norfolk, EEUU).

Su resumen

The Marching Cubes algorithm is a well known and widely used approach for extracting a triangulated isosurface from a three-dimensional rectilinear grid of uniformly sampled data values. The algorithm relies on a large manually constructed table which exhaustively enumerates all possible patterns in which the isosurface can intersect a cubical cell of the grid. For each pattern the table con- tains the local connectivity of the triangles. The construction of this table is labor intensive and error prone. Indeed, the original paper allowed for topological holes in the surface. This problem was later fixed by several authors, however a formal proof of correctness to our knowledge was never presented. In our opinion the most reliable approach to constructing a formal proof for this algorithm is to write a computer program which checks that all the entries in the table satisfy some sufficient condition of correctness. In this paper we present our formal proof which follows this approach, developed with the Coq proof assistant software. The script of our proof can be executed by Coq which verifies that the proof is logically correct, in the sense that its conclusions indeed logically follow from the assumptions. Coq offers a number of helpful features that automate proof development. However, Coq cannot check that the development corresponds to the problem we wish to solve, therefore, this correspondence is elaborated upon in this paper. Our complete Coq development is available online.

El trabajo se presentará en octubre en el 22nd International Meshing Roundtable.