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.