Login Barrapunto
Premio Turing 2007
Riviera nos cuenta: «La ACM ha anunciado el Premio Turing 2007, que ha sido otorgado a
Edmund M. Clarke,
E. Allen Emerson y
Joseph Sifakis por su trabajo pionero en un método automatizado para encontrar errores de diseño en software y hardware. Es la primera vez que el premio recae en un científico griego, Sifakis (o francés, si se considera su lugar de trabajo).»
Este hilo ha sido archivado.
No pueden publicarse nuevos comentarios.
Y recuerda: Los comentarios que siguen pertenecen a las personas que los han enviado. No somos responsables de los mismos.
ironías del destino...
(Puntos:2, Interesante)( http://barrapunto.com/ | Última bitácora: Miércoles, 23 Julio de 2008, 17:19h )
no es de extrañar que el hecho de trabajar en francia le haya facilitado el premio, además de facilitarle el acceso al "primer mundo de la ciencia". una ligera búsqueda sobre las "divisiones de la producción y publicación científica"... aquí [elpais.com]
ciao!
slashdot ain't what it used to be: para entendernos, barrapunto ya no es lo que era!!!
Otro hype tecnológico
(Puntos:2, Interesante)Como dice uno de los posts [slashdot.org] en el hilo de Slashdot, los métodos de validación de modelos sólo trasladan la problemática de validar que un programa es correcto, a la problemática de validar que un diseño, descrito en un lenguaje tan complejo como un lenguaje de programación, es correcto.
No hay ningún método automatizado y general para encontrar errores de diseño en el software. Si así fuese, podríamos coger los fuentes del kernel de Linux, traducirlos al lenguaje formal de especificación de modelos mediante un compilador automático, y comprobar si tiene errores o no mediante uno de estos programas también automáticos. Obviamente esto es imposible, porque en algún lado del proceso hace falta algo que diga qué es correcto y qué no. Sólo sabríamos que el kernel de Linux es correcto según su diseño (cada programa siempre es un modelo perfecto de si mismo), pero no sabríamos si su diseño es correcto o no.
Como mucho estos métodos pueden servir para validar problemas sencillos, algoritmos, o chips con un dominio de valores de entrada y salida perfectamente conocido, donde la solución "trivial" es computable. Quien haya leído algo sobre complejidad algorítmica sabrá que cada programa tiene una implementación trivial pero no factible que es simplemente una matriz o un array donde a cada valor posible del dominio de entrada se le asigna un valor de salida. Hemos descubierto la pólvora.
Lo malo es que ahora vendrán toda la panda de filósofos de software, estos que no han hecho un programa en su vida, a afirmar que es posible validar los diseños de los programas sin necesidad de construirlos primero, mediante su especificación con lenguajes gráficos de modelado , jeroglíficos o lenguajes matemáticos que son tan complejos o más que lenguajes de programación convencionales, lo que les permitirá seguir viviendo del cuento unos años más a todos estos charlatanes de las herramientas CASE, la generación automática de programas sin programadores, y demás hypes tecnológicos.
Re:Intrusos
(Puntos:1)Re:Intrusos
(Puntos:1)( Última bitácora: Jueves, 09 Febrero de 2006, 18:59h )
a) Los enemigos del intrusismo.
b) O en realidad, es un odio mucho mas profundo... Los que hayan estudiado ingeniería en informática.
Porque me parece que tienes una frustración o algo, siempre repitiendo las mismas obviedades. Yo creo que realmente te sientes excluido, pero es mas bien un sentimiento interno tuyo, que una exclusion del resto de titulados hacia tí. Es como que justificas tu frustración creando un enemigo fantasma para calmar tu complejo de inferioridad.