397 investigadores han obtenido una beca ERC Starting Grant. Tras la primera convocatoria de propuestas del nuevo programa de I+D de la UE, Horizonte Europa, se invertirán 619 millones de euros en la convocatoria de 2021, en proyectos excelentes ideados por científicos y académicos.
La investigadora del Instituto IMDEA de Software, Niki Vazou, ha recibido una ERC Starting Grant por valor de 1,5 millones de euros que le ayudará a poner en marcha su propio proyecto, formar un equipo y perseguir sus mejores ideas.
El projecto CRETE
Los tipos de refinamiento son una prometedora tecnología de verificación que en la última década se ha extendido a los lenguajes convencionales (por ejemplo, Haskell, C, Ruby, Scala y la familia ML) para verificar propiedades sofisticadas de aplicaciones del mundo real, por ejemplo, la seguridad de los protocolos criptográficos, el uso de la memoria y los recursos, y la seguridad de la web.
El punto débil de los tipos de refinamiento es que no cumplen los estándares de solidez establecidos por los demostradores de teoremas. Un sistema de verificación sólido sólo acepta como seguros aquellos programas que nunca violan sus especificaciones. Los verificadores de tipos de refinamiento (por ejemplo, Liquid Haskell, F* e Stainless) informan de aproximadamente cinco errores de solidez al año, frente a sólo uno informado por el comprobador de teoremas Coq. Esta rareza de los errores de solidez en Coq no es sorprendente, ya que Coq está diseñado para comprobar mecánicamente las pruebas matemáticas. Sin embargo, la receta de diseño de solidez de Coq no puede aplicarse directamente a los verificadores de tipo de refinamiento que pretenden verificar de forma práctica los programas del mundo real.
El objetivo de CRETE es diseñar un sistema de refinamiento de tipos sólido y práctico. Este es un objetivo ambicioso que implica el desarrollo de un sistema de verificación que sea tan práctico como los tipos de refinamiento y que construya pruebas matemáticas comprobadas por la máquina. El sistema se implementará en sistemas de refinamiento de tipos para lenguajes convencionales (es decir, Haskell y Rust) y se evaluará en código del mundo real, como aplicaciones web y protocolos criptográficos.
“Financiado por la Unión Europea. Sin embargo, los puntos de vista y las opiniones expresadas son únicamente los del autor o autores y no reflejan necesariamente los de la Unión Europea o el Consejo Europeo de Investigación. Ni la Unión Europea ni la autoridad que los ha concedido pueden ser considerados responsables de los mismos.” Referencia: 101039196.
