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