Uno de los problemas centrales hoy en día en la Informática aplicada es asegurar que los programas son correctos, es decir, hacen lo que se espera de ellos. Las dificultades para aumentar la fiabilidad de los sistemas informáticos son enormes y tienen múltiples fuentes: desde aspectos psicológicos hasta otros relacionados con la complejidad de los sistemas, pasando por las ambigüedades del lenguaje natural.
Por ello, en lugar de atacar el problema general (lo que sería demasiado ambicioso en este momento), la investigación práctica se dirige a temas particulares, de los que se espera obtener una mejor aproximación a los problemas de la informática en la vida cotidiana.
La investigación doctoral de Jesús Mª Aransay se ha dirigido a unos sistemas informáticos muy específicos: aquellos dedicados al cálculo científico que se basan en el lenguaje de las matemáticas. Incluso en este ámbito restringido, los desafíos son importantes y necesitan del recurso de técnicas de Inteligencia Artificial.
En la tesis se ha utilizado una herramienta de razonamiento mecanizado (llamada Isabelle) para asegurar la corrección de programas que permiten el cálculo en Topología Algebraica. Las conclusiones señalan una vía que puede ser fructífera para aumentar la fiabilidad de los sistemas informáticos dedicados al cálculo científico, indicando los problemas abiertos en lo que será necesario seguir investigando.
Los resultados de la tesis, co-dirigida por el profesor de la Universidad Técnica de Munich Clemens Ballarin, han sido presentados en diversos congresos internacionales relacionados con el Cálculo Simbólico y la Inteligencia Artificial, han dado lugar a varias publicaciones.