Universidad de La RiojaCampus Iberus    
 
 
Principal Office 365 Correo-web Directorio Mapa web Contacto
Información para
Estudiantes
Admisión y Matrícula
Foreign students
Antiguos alumnos
Empresas
Visitantes
PDI/PAS
Información sobre
Universidad de La Rioja
Estudios
Campus Virtual
Investigación
Portal de Investigación
Escuela Máster y Doctorado
Centro de Idiomas
Facultades y Escuelas
Departamentos
Administración y Servicios
Biblioteca
Fundación de la UR
Fundación Dialnet
Portal de transparencia
Defensoría Universitaria
Unidad de Igualdad
Oficina de Sostenibilidad
Sede electrónica
Actualidad
Noticias
Agenda
Congresos y jornadas
Plazas PDI/PAS
Perfil del contratante
Boletines y publicaciones
 
Sede Electrónica
Tablón Electrónico
Cita Previa
Oficina del Estudiante
 
 
facebook Twitter You Tube Flickr
pinterest linkedin instagram
 
Noticias

Tesis sobre la verificación de algoritmos y seguridad informática
Jose Divasón Mallaragay obtiene el grado de doctor

7 de julio de 2016
Jose Divasón se doctora con una tesis sobre la verificación de algoritmos para mejorar la seguridad informática.

Jose Divasón Mallagaray ha obtenido el grado de doctor por la Universidad de La Rioja tras la defensa de su tesis Formalisation and execution of Linear Algebra: theorems and algorithms, por la que ha logrado la calificación de sobresaliente 'cum laude' con mención internacional al título.

Desarrollada en el Departamento de Matemáticas y Computación de la Universidad de La Rioja, esta tesis doctoral ha sido dirigida por Julio Rubio García y Jesús M.ª Aransay Azofra.

La tesis ha dado lugar a ocho publicaciones científicas y seis conferencias internacionales, y parte de ella se ha desarrollado en estancias de investigación en la Technische Universität München (Alemania) y en la Universität Innsbruck (Austria).

El desarrollo de software es propenso a errores. A veces, los ordenadores se cuelgan y los smartphones se reinician solos. Normalmente estos fallos -conocidos como 'bugs'- suelen causar simplemente un inconveniente.

Sin embargo en sistemas críticos (como, por ejemplo, en bancos, medios de transporte o dispositivos médicos), estos fallos pueden tener un enorme impacto económico, dañar considerablemente la reputación de las empresas y lo que es peor, podrían llegar a causar pérdidas humanas. Por ello es necesario verificar software.

En esta tesis se aborda la verificación formal de algoritmos, concretamente en el marco de álgebra lineal, a través del demostrador interactivo de teoremas Isabelle/HOL; y, para ello, se ha creado una infraestructura donde es posible formalizar, ejecutar, refinar y conectar los algoritmos con su significado matemático.

Dicha infraestructura es utilizada para generar código verificado en lenguajes de programación funcional de cuatro conocidos algoritmos y sus aplicaciones (Gauss-Jordan, descomposición QR, forma escalonada y forma normal de Hermite).

Además, no solo se ha buscado la generación de código verificado, sino que se ha trabajado para que el código sea además eficiente y útil en casos reales, como en el estudio de imágenes biomédicas o en el cálculo de determinantes que algunos programas comerciales realizaban incorrectamente.

Por último, también se han presentado unos experimentos sobre una formalización del modelo simplicial propuesto por Voevodsky (ganador de la medalla Fields en 2002) para los fundamentos de las matemáticas conocidos como Univalent Foundations.

comunicacion@adm.unirioja.es


Jose Divason Mallagaray
Ampliar y descargar imagen
Noticias relacionadas

Formath, proyecto europeo sobre seguridad informática

Seguridad informática para análisis neurológicos

María Poza obtiene el título de doctora por la UR

Premio 'Software Presentatión' del ISSAC 2019
Sobre este web | © Universidad de La Rioja