Innovating Works

TIN2008-05624

Financiado
DESARROLLO DE SOFTWARE VERIFICABLE Y EFICIENTE
LA IMPORTANCIA DEL SOFTWARE AUMENTA CADA DIA, DEBIDO EN PARTE A SUPRESENCIA EN UN NUMERO CADA VEZ MAYOR DE DISPOSITIVOS, YFRECUENTEMENTE CONTROLANDO APLICACIONES DE SEGURIDAD CRITICA, POR LOTANTO, ES CRUCIAL DISPONER DE LOS MEDIO... LA IMPORTANCIA DEL SOFTWARE AUMENTA CADA DIA, DEBIDO EN PARTE A SUPRESENCIA EN UN NUMERO CADA VEZ MAYOR DE DISPOSITIVOS, YFRECUENTEMENTE CONTROLANDO APLICACIONES DE SEGURIDAD CRITICA, POR LOTANTO, ES CRUCIAL DISPONER DE LOS MEDIOS NECESARIOS PARA DESARROLLAR,DE FORMA SIMPLE, SOFTWARE FIABLE Y EFICIENTE, EL OBJETIVO FINAL DEESTE PROYECTO ES EL DESARROLLO DE LOS METODOS Y LAS HERRAMIENTASNECESARIAS PARA LA GENERACION DE SOFTWARE VERIFICABLE Y EFICIENTE,LAS TECNOLOGIAS RELACIONADAS CON LOS LENGUAJES DE PROGRAMACION HANSIDO OBJETO DE NUMEROSOS ESTUDIOS EN LAS ULTIMAS DECADAS, LO QUE HADADO LUGAR A IMPORTANTES AVANCES EN LAS AREAS DE DISEÑO DE LENGUAJES,TRANSFORMACION Y VERIFICACION DE PROGRAMAS, ETC,, ASI COMO EN TECNICASEMERGENTES TALES COMO EL CODIGO CON DEMOSTRACION, UNA TECNOLOGIAESENCIAL PARA ESTOS AVANCES ES EL ANALISIS ESTATICO DE PROGRAMAS, AMENUDO FORMALIZADO EN TERMINOS DE INTERPRETACION ABSTRACTA --UNENFOQUE BASADO EN LA SEMANTICA QUE PERMITE INFERIR UNA GRAN VARIEDADDE PROPIEDADES SOBRE EL COMPORTAMIENTO DE LOS PROGRAMAS, LAS CUALESSON DE GRAN UTILIDAD TANTO PARA PODER ASEGURAR LA CORRECCION COMO PARAOBTENER EFICIENCIA, Y DE UN MODO QUE ES A LA VEZ RIGUROSO Y DE GRANAPLICABILIDAD PRACTICA, ESTAS PROPIEDADES INCLUYEN POR EJEMPLOAPROXIMACIONES SEGURAS SOBRE EL USO DE DIFERENTES RECURSOS TALES COMOLA COMPLEJIDAD DEL PROGRAMA O EL USO DE MEMORIA, EL NIVEL DE MADUREZACTUAL DE ESTAS TECNICAS PERMITE, TAL COMO SE PROPONE EN ESTEPROYECTO, APLICARLAS A PROGRAMAS REALISTAS, OTRO FACTOR DE MOTIVACIONIMPORTANTE PARA ESTA PROPUESTA ES EL PARALELISMO, DEBIDO AL DECLIVE DELA LEY DE MOORE, LAS ARQUITECTURAS DE PROCESADOR MULTI-NUCLEO SON CADAVEZ MAS POPULARES, Y LAS PREDICCIONES INDICAN QUE, EN LOS PROXIMOSAÑOS, SE INCLUIRAN CADA VEZ MAS NUCLEOS POR PROCESADOR PARA MEJORAR ELRENDIMIENTO (EN VEZ DE AUMENTAR LA FRECUENCIA EN PROCESADORESESCALARES), LA EXPLOTACION AUTOMATICA Y FIABLE DE ESTE PARALELISMOINHERENTE EN EL HARDWARE DE UNA MANERA EFICIENTE ES ACTUALMENTE UNRETO DE GRAN RELEVANCIA PRACTICA, EN ESTE CONTEXTO, ES INTERESANTERESALTAR QUE LAS TECNICAS DE ANALISIS Y LAS PROPIEDADES A INFERIR QUEUTILIZAN LOS COMPILADORES PARALELIZANTES SON LAS MISMAS O SIMILARES ALAS MENCIONADAS ANTERIORMENTE,NUESTRA PROPUESTA REUNE A INVESTIGADORES DE LA UPM Y UCM (ASI COMO AUN NUMERO DE INVESTIGADORES EXTRANJEROS CLAVE) QUE CUENTAN CON UNRECONOCIDO PRESTIGIO INTERNACIONAL EN LAS AREAS DE ANALISIS ESTATICO,VERIFICACION DE PROGRAMAS Y PARALELIZACION AUTOMATICA, CONSIDERAMOSQUE EL PROYECTO, EN CASO DE SER APROBADO, PERMITIRA UN ESFUERZOINVESTIGADOR ADICIONAL QUE DARA COMO FRUTO RESULTADOS CIENTIFICOS YTECNICOS DE MUCHO MAYOR IMPACTO QUE LOS QUE DICHOS INVESTIGADORESPODRIAN CONSEGUIR POR SEPARADO, EL PROYECTO SE CENTRA EN ELDESARROLLO DE TECNOLOGIAS FUNDAMENTALES, APLICABLES A DIFERENTESPARADIGMAS Y LENGUAJES DE PROGRAMACION, EN CONCRETO, LOSPARTICIPANTES TRABAJARAN SOBRE (I) SU PROPIO ENTORNO DE DESARROLLO,CIAO, CON LA INTENCION DE MAXIMIZAR LOS PROGRESOS CIENTIFICOS; CIAODISPONE DE UNA SEMANTICA DECLARATIVA QUE PERMITE CONCENTRARSE EN LOSASPECTOS REALMENTE IMPORTANTES DE LOS PROBLEMAS A RESOLVER, Y (II)CODIGO DE BYTE DE JAVA, PARA MAXIMIZAR EL IMPACTO DE LAS HERRAMIENTASY TECNICAS DESARROLLADAS, DADO QUE ESTE TIPO DE CODIGO JUEGA EN LAACTUALIDAD UN PAPEL CRUCIAL EN MUCHAS APLICACIONES, INCLUIDAS LAS QUEIMPLICAN MOVILIDAD DE CODIGO, Análisis Estático\Verificación\Desarrollo de Software\Optimización\Paralelización Automática\Interpretación Abstracta\Código con Demostración ver más
01/01/2008
UPM
505K€
Perfil tecnológico estimado

Línea de financiación: concedida

El organismo AGENCIA ESTATAL DE INVESTIGACIÓN notifico la concesión del proyecto el día 2008-01-01
Presupuesto El presupuesto total del proyecto asciende a 505K€
Líder del proyecto
UNIVERSIDAD POLITÉCNICA DE MADRID No se ha especificado una descripción o un objeto social para esta compañía.
Total investigadores 3944