Ponente: David Rosenblueth (IIMAS-UNAM)
03/05/2011
de 12:00 a 13:00
Dónde Salón "Graciela Salicrup"
Resumen:
En los años 70 había el proyecto de desarrollar técnicas para demostrar que todo programa de computadora estaba correcto. Dicho proyecto fracasó, por supuesto, pero dio origen a una serie de herramientas llamadas "verificación de modelos", que resuelven una versión suavizada la idea original.
La verificación de modelos típicamente funciona sólo para sistemas finitos, y sólo demuestra que cierto aspecto parcial de su comportamiento está correcto. A pesar de estas limitaciones (o quizás gracias a ellas), los verificadores de modelos han tenido un impacto en la industria pues pueden verificar sistemas enormes, con 10^50 estados o más. Actualmente, los verificadores de modelos se emplean sobre todo en el diseño de circuitos digitales.
Esta plática va a tratar de las posibilidades y los obstáculos en la aplicación de la verificación de modelos en otra área: el estudio de redes genéticas.
Temas: