Proof Pearl: A Formal Proof of Dally and Seitz’ Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks

PorJosé A. Alonso

Se ha publicado un nuevo artículo de formalización: Proof Pearl: A Formal Proof of Dally and Seitz’ Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks

Los autores del artículo son Freek Verbeek y Julien Schmaltz de la Universiad de Radboud en Nimega (en neerlandés: Nijmegen), Paises Bajos.

El artículo se publicó ayer (18 de Septiembre de 2010) en el Journal of Automated Reasoning.

Una versión preliminar del artículo puede leerse aquí y el código ACL2 correspondiente puede obtenerse aquí

El artículo es una demostración en ACL2 de una condición necesaria y suficiente para enrutamiento sin estancamiento introducida por William J. Dally y Charles L. Seitz en su artículo Deadlock Free Message Routing in Multiprocessor Interconnection Networks de 1987.
Read More “Proof Pearl: A Formal Proof of Dally and Seitz’ Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks”

Trabajo de Lógica Computacional en Cambridge

PorJosé A. Alonso

Se ha anunciado la oferta de plazas de trabajo en la Universidad de Cambridge.

El trabajo se realizará dentro del proyecto EPRSC Semantic Foundations for Real-World Systems. Entre sus objetivos se encuentra la verificación de la compilación de lenguajes concurrentes, para lo que se requiere conocimiento de verificación de programas y de sistemas de razonamiento.

El director del proyecto es Peter Sewell

Premios HVC de verificación a la comunidad SMT (Satisfiability Modulo Theories)

PorJosé A. Alonso

Los premios HVC (Haifa Verification Conference) se conceden a los trabajos más prometedores en la campos de verificación y prueba de software y hardware. Este año los premios HVC 2010 le han sido otorgados a los promotores de la comunidad de satisfacibilidad módulo teorías (en inglés, Satisfiability Modulo Theories (SMT) personalisados en

Read More “Premios HVC de verificación a la comunidad SMT (Satisfiability Modulo Theories)”

Anuncio: Trace-based verification of imperative programs with I/O

PorJosé A. Alonso

Gregory Malecha, Greg Morrisett y Ryan Wisnesky han publicado el artículo Trace-based verification of imperative programs with I/O en el Journal of Symbolic Computation. Una versión del artículo puede leerse aquí.

El resumen del artículo es

In this paper we demonstrate how to prove the correctness of systems implemented using low-level imperative features like pointers, files, and socket I/O with respect to high level I/O protocol descriptions by using the Coq proof assistant. We present a web-based course gradebook application developed with Ynot, a Coq library for verified imperative programming. We add a dialog-based I/O system to Ynot, and we extend Ynot’s underlying Hoare logic with event traces to reason about I/O and protocol behavior. Expressive abstractions allow the modular verification of both high level specifications like privacy guarantees and low level properties like data structure pointer invariants.

Los autores son miembros del Grupo de Lenguajes de Programación de la Universidad de Harvard.

Este artículo está relacionado con el proyecto SAFE (Semantically Aware Foundation Environment) comentado en una entrada anterior.

Cero elevado a cero y errores informáticos

PorJosé A. Alonso

Es muy frecuente los errores que se comenten al calcular el valor de “cero elevado a cero”. De esta forma, hay quienes piensan erróneamente que es un operación “prohibida”, que es una indeterminada o que su valor es 0.

En el artículo Cero elevado a la cero de Gustavo Piñeiro se explica detalladamente porqué cero elevado a cero es igual a uno.

Los errores sobre cero elevado a cero no sólo se dan entre los humanos, sino que también se dan en los sistemas informáticos. Maxima lo calcula erróneamente como se puede observar en la siguiente sesión
Read More “Cero elevado a cero y errores informáticos”