Resumen
El objetivo de este proyecto es el desarrollo de nuevas técnicas y herramientas automáticas que permitan garantizar la confiabilidad del software, contribuyendo a erradicar los fallos que, de otra forma, podrían conducir a vulnerabilidades de seguridad y/o errores de cómputo. El proyecto plantea un programa integrado de investigación en técnicas formales para la calidad del software, una tecnología con fuerte base matemática que se aplica al análisis, modelado, verificación, síntesis, aprendizaje, depuración y optimización automática de sistemas complejos.
El presente proyecto persigue investigar una amplia variedad de tecnologías orientadas a asegurar la confiabilidad del software, reuniendo un equipo consolidado con 30 años de trayectoria de investigación en el área y enfocándose la investigación hacia las siguientes técnicas, herramientas y aplicaciones:
(a) la formulación de nuevas técnicas de razonamiento formal con base lógica y algebraica (reglas de reescritura, resolución de restricciones, satisfacibilidad módulo teoríaas, interpretación abstracta,técnicas simbólicas, etc).
(b) el desarrollo de técnicas y herramientas software para el análisis, modelado, verificación, síntesis, depuración y optimización de sistemas heterogéneos complejos con especificaciones profundas.
(c) el análisis de las teorías lógicas (especificaciones) que pueden extraerse a partir de modelos de aprendizaje automático y su aplicación a tareas en las que coexistan especificaciones formales de protocolos junto con ejemplos.
(d) el análisis profundo de la seguridad y confiabilidad de sistemas software complejos.
