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.

El problema de la igualdad de los bordes de los árboles binarios (sameFringe)

PorJosé A. Alonso

Dos árboles binarios tienen iguales los bordes si tienen exactamente
las mismas hojas leídas de izquierda a derecha, independientemente de
nodos interiores. Por ejemplo,

Los bordes de los árboles 1 y 2 son iguales, aunque tiene distintas
estructuras internas. El árbol 3 no tiene el mismo borde que el 1 o
el 2, debido al nodo 4. El árbol 4 tampoco tiene el mismo borde que
el 1 debido al orden en que se leen las hojas.

El problema de la igualdad de los bordes de los árboles binarios
(samefringe, en inglés) consiste en decidir si dos árboles tienen los bordes iguales.
Read More “El problema de la igualdad de los bordes de los árboles binarios (sameFringe)”

Trabajo de Lógica Computacional en las Universidades de Pensilvania, Harvard y Northeastern

PorJosé A. Alonso

Se ha anunciado la oferta de plazas postdoctorales en la Universidad de Pensilvania, la Universidad de Harvard y la Universidad Northeastern.

El trabajo se desarrollará dentro del proyecto SAFE (Semantically Aware Foundation Environment).

SAFE es parte del proyecto CRASH (Clean-Slate Design of Resilient, Adaptive, Secure Hosts)

CRASH es un gran proyecto financiado por la DARPA (Defense Advanced Research Projects Agency) cuyo objetivo es el diseño de nuevos sistemas computacionales que sean muy resistentes a los ciberataques. Se desea diseñar los niveles de hardware, sistemas operativos y lenguajes de programación poniendo el énfasis en la simplicidad, seguridad y verificabilidad de todos los niveles.

Las áreas de trabajo son lenguajes de programación, verificación formal, sistemas operativos y diseño de hardware.

Anuncio: Reducing the size of resolution proofs in linear time

PorJosé A. Alonso

Se ha publicado el artículo Reducing the size of resolution proofs in linear time en la revista International Journal on Software Tools for Technology Transfer (STTT).

Una versión del artículo puede leerse aquí

Los autores del artículo son Omer Bar-Ilan, Oded Fuhrmann, Shlomo Hoory, Ohad Shacham y Ofer Strichman. Los tres primeros trabajaban en IBM R&D Labs in Israel y el cuarto en Technion – Israel Institute of Technology.

El resumen del artículo es
Read More “Anuncio: Reducing the size of resolution proofs in linear time”