Portada arrow NO-ticias arrow Model Checking y los Premios Turing 2007
Model Checking y los Premios Turing 2007
lunes, 31 de marzo de 2008

El pasado mes de febrero se dieron a conocer los galardonados con el premio Turing 2007. Este premio, otorgado por la Association for Computer Machinery (ACM) está considerado como el más prestigioso del campo de la informática y la computación.

Aunque la presentación oficial del premio será el 21 de Junio de 2008, ya se conoce el nombre de las personas en las que recaerá. En esta ocasión, son tres: Edmund M. Clarke, E. Allen Emerson y Joseph Sifakis.

El motivo por el cual se les otorga es premio es "por su papel en el proceso de convertir el Model Checking en una tecnología de verificación altamente efectiva ampliamente adoptada en las industrias del hardware y del software".

 

El Model Checking es un sistema de verificación formal. En principio, y a pesar de lo que reza la dedicatoria del premio, está orientado principalmente a hardware. En el software, debido a su naturaleza y a otros problemas inherentes que plantea, aunque pueda aplicarse en determinados casos, no tiene tanta utilidad práctica. La técnica consiste básicamente en representar el comportamiento de una pieza de hardware con un grafo dirigido, en el cual, los nodos representan estados del hardware y los arcos transiciones entre ellos. A cada nodo se le asocia una serie de reglas escritas en forma de proposiciones de lógica temporal. La matemática desarrollada por los tres galardonados incluye búsquedas y otros cálculos sobre estos grafos que permiten deducir propiedades acerca del modelo, y por ende, del hardware que está representando. En particular y especialmente, esa matemática debe decirnos de manera automática si el modelo satisface correctamente una serie de requerimientos. Además del funcionamiento básico del modelo, los galardonados están involucrados en el desarrollo de varios tipos de optimizaciones y algoritmos mejorados sobre las técnicas básicas.

 

 

Para saber más:

 

-La página de cada uno de ellos. (en inglés)

 

Joseph Sifakis

Joseph Sifakis External link

E. Allen Emerson

E. Allen Emerson External link

Edmund M. Clarke

Edmund M. Clarke External link

 

-Nota de prensa de la ACM External link acerca de la concesión del premio y breve descripción profesional de cada uno de los galardonados. (en inglés)

 

-Model checking en wikipedia en español External link.

-Model checking en wikipedia en inglés External link (algo más completo).

 

-Una introducción al Model Checking External link en embedded.com. (en inglés)

 


Comentarios
Añadir nuevo
+/-
Escribir comentario
Nombre:
Email: (opcional)
 
Website: (opcional)
Título:
 
:angry::0:confused::cheer:B):evil::silly::dry::lol::kiss::D:pinch:
:(:shock::X:side::):P:unsure::woohoo::huh::whistle:;):s
:!::?::idea::arrow:
 
Por favor introduce el código anti-spam que puedes leer en la imagen.
Por favor, sólo comentarios relacionados con la temática del artículo
Comentarios ofensivos contra personas o instituciones, carentes de contenido o que contengan publicidad serán eliminados.

3.21 Copyright (C) 2007 Alain Georgette / Copyright (C) 2006 Frantisek Hliva. All rights reserved."

 
←Artículo anterior   Artículo siguiente→

Artículos relacionados

No se encontraron artículos relacionados

¿Quién está en línea?

 web tracker

Suscríbete

RSS feed Sindicación RSS

(¿Qué es la sindicación RSS?)


Suscribir por e-mail

¿Dónde estoy?

Estás en La tecla de ESCAPE, un sitio web personal en el que nos gusta hablar de algoritmos, informática, tecnología, ciencia, ingeniería, internet... y cualquier tontería que se nos ocurra. El punto de vista de nuestros artículos técnicos suele ser muy básico, así que a menudo adoptamos grandes simplificaciones. (Más...-Términos de uso)