José Meseguer Guaita es un informático español , y profesor de la Universidad de Illinois en Urbana-Champaign . Dirige el Laboratorio de Métodos Formales y Lenguajes Declarativos de la universidad.
José Meseguer obtuvo su doctorado en matemáticas en 1975 con una tesis titulada Recursión primitiva en categorías de modelos dirigida por Michael Pfender en la Universidad de Zaragoza , tras la cual realizó trabajos postdoctorales en la Universidad de Santiago de Compostela y la Universidad de California en Berkeley . En 1980 se incorporó al Laboratorio de Ciencias de la Computación de SRI International , convirtiéndose finalmente en Científico Principal y Jefe del Grupo de Lógica y Lenguajes Declarativos . Se incorporó a la Universidad de Illinois en 2001 y actualmente es profesor de Ciencias de la Computación, donde dirige su Laboratorio de Métodos Formales y Lenguajes Declarativos.
Ha trabajado particularmente en el diseño e implementación de lenguajes declarativos, incluidos OBJ y Maude , así como en la reescritura de lógica. [3]
Recibió la beca Europa de Métodos Formales de 2019 . [4] La cita del premio [5] dice:
Por todos sus logros académicos y su liderazgo e impacto en la comunidad de métodos formales , presentamos al Prof. José Meseguer, FME Fellow 2019. El Prof. Meseguer es un investigador líder con contribuciones fundamentales en muchos campos de la informática teórica y más allá: desde la lógica general hasta los algoritmos de visión para robots . Su trabajo se caracteriza por la innovación, la elegancia conceptual y el rigor, combinados con la aplicabilidad práctica.
El Prof. José Meseguer es conocido por su investigación fundamental sobre especificación algebraica , concurrencia , reescritura , lógica y seguridad informática . La investigación de nuestro nuevo becario se caracteriza por lógicas computacionales prácticas, simples e intuitivas y métodos y herramientas de análisis asociados. Los resultados de la investigación se han aplicado con éxito a sistemas complejos de última generación en diversos ámbitos.
Su trabajo en seguridad informática es especialmente significativo. Su formalización de la no interferencia es uno de los conceptos más conocidos en seguridad informática, ampliamente utilizado tanto por académicos como por profesionales. Su artículo sobre políticas de seguridad y modelos de seguridad es uno de los artículos más citados en seguridad informática (con casi 2500 citas de Google Scholar ).
Ha trabajado en el diseño e implementación de varios lenguajes declarativos , incluidos OBJ y Maude , en especificación formal y técnicas de verificación , en teoría de concurrencia , en enfoques formales para la especificación orientada a objetos, en software y arquitecturas paralelas para lenguajes declarativos, y en la Fundamentos lógicos de la informática utilizando la lógica ecuacional , la reescritura de la lógica y la teoría de la lógica general.
Es el inventor de la reescritura de la lógica y el principal desarrollador de Maude. Su contribución fundamental a los métodos formales ha sido la invención y desarrollo de la reescritura como una lógica computacional y un marco semántico expresivo e intuitivo para sistemas concurrentes. En particular, el conjunto de herramientas Maude es una práctica herramienta de reescritura de alto rendimiento.
Un resultado importante es la demostración de que la reescritura de la lógica es un modelo natural y simple de concurrencia. La simplicidad y expresividad de la reescritura de la lógica, tal como se implementa en Maude, ha dado como resultado la especificación y el análisis de una amplia gama de sistemas, incluidos modelos de computación , diferentes lógicas y lenguajes de programación y modelado industrial .
También ha hecho contribuciones fundamentales al análisis formal de sistemas distribuidos , combinando razonamiento basado en estados y basado en acciones en lógica temporal ; combinar la reescritura con la resolución SMT ; y proporcionar algoritmos de resolución de SMT teóricos genéricos que se pueden aplicar no solo a teorías fijas predefinidas, sino a cualquier teoría que satisfaga ciertas propiedades. Las contribuciones de investigación más recientes incluyen sistemas ciberfísicos , computación en la nube y sistemas biológicos .
Su enfoque científico se describe mejor con la máxima "la belleza es nuestro negocio". No tiene miedo de aventurarse en dominios alejados de lo que pensaríamos que son sus zonas de confort; De hecho, disfruta la oportunidad de imponer rigor en otros campos y enfrentar nuevos desafíos que inspiren nuevos desarrollos teóricos.
El testimonio de sus amigos y colegas de que intenta mantener los más altos estándares éticos y científicos en su investigación y en su trato con colegas, estudiantes y otras personas a su alrededor. Los nuevos estudiantes son tratados con la misma cortesía que los investigadores destacados. Esto se refleja en el hecho de que muchos antiguos alumnos continúan colaborando cuando se convierten en investigadores de mayor nivel.
Es notablemente generoso al compartir y discutir las muchas ideas que emanan de su mente fértil, y es genuinamente curioso y agradecido por otras opiniones. Este espíritu de colaboración también se ve reflejado en el hecho de que tiene 132 coautores incluidos en DBLP . A pesar de ser uno de los científicos informáticos más destacados de nuestra generación, muchos de sus colaboradores lo consideran, ante todo, un amigo notablemente leal y verdadero.
Fue admitido como miembro de ACM en 2020 "para el desarrollo de métodos lógicos para el diseño y verificación de sistemas computacionales". [6] [7]