José Meseguer Guaita is a Spanish computer scientist, and professor at the University of Illinois at Urbana–Champaign. He leads the university's Formal Methods and Declarative Languages Laboratory.

Career

José Meseguer obtained his PhD in mathematics in 1975 with a thesis titled Primitive recursion in model categories under Michael Pfender at the University of Zaragoza, after which he did post-doctoral work at the University of Santiago de Compostela and the University of California at Berkeley. In 1980 he joined the Computer Science Laboratory at SRI International, eventually becoming a Principal Scientist and Head of the Logic and Declarative Languages Group. He joined the University of Illinois in 2001 and currently is Professor of Computer Science, where he leads their Formal Methods and Declarative Languages Laboratory.

He has worked particularly on the design and implementation of declarative languages, including OBJ and Maude, as well as rewriting logic.^[3]

He was awarded the 2019 Formal Methods Europe Fellowship.^[4] The award citation^[5] reads,

For all his academic achievements, and his leadership and impact on the formal methods community, we present Prof. José Meseguer, the 2019 FME Fellow. Prof. Meseguer is a leading researcher with seminal contributions in many fields of theoretical computer science and beyond: from general logics to vision algorithms for robots. His work is characterised by innovation, conceptual elegance, and rigor, combined with practical applicability.

Prof. José Meseguer is known for his seminal research on algebraic specification, concurrency, rewriting, logic, and computer security. The research of our new Fellow is characterised by practical, simple, and intuitive computational logics and associated analysis methods and tools. The research results have been successfully applied to complex state-of-the-art systems in diverse domains.

His work on computer security is especially significant. His formalisation of noninterference is one of the most well-known concepts in computer security, extensively used by both academics and practitioners. His paper on security policies and security models is one of the most cited papers in computer security (with nearly 2,500 Google Scholar citations).

He has worked on the design and implementation of several declarative languages, including OBJ and Maude, on formal specification and verification techniques, on concurrency theory, on formal approaches to object-oriented specification, on parallel software and architectures for declarative languages, and on the logical foundations of Computer Science using equational logic, rewriting logic, and the theory of general logics.

He is the inventor of rewriting logic and the main developer of Maude. His fundamental contribution to formal methods has been the invention and development of rewriting as an expressive and intuitive computational logic and semantic framework for concurrent systems. In particular, the Maude toolset is a practical high-performance rewriting tool.

An important outcome is the demonstration that rewriting logic is a natural and simple model for concurrency. The simplicity and expressiveness of rewriting logic, as implemented in Maude, have resulted in the specification and analysis of a wide range of systems, including models of computation, different logics, and industrial programming, and modelling languages.

He has also made fundamental contributions to the formal analysis of distributed systems, combining state-based and action-based reasoning in temporal logic; combining rewriting with SMT solving; and providing theory-generic SMT solving algorithms that can be applied not only to fixed predefined theories, but to any theory that satisfies certain properties. More recent research contributions include cyber-physical systems, cloud computing, and biological systems.

His scientific approach is best described by the dictum ‘‘beauty is our business’’. He is not afraid of venturing into domains far away from what we would think are his comfort zones; he actually relishes the opportunity to impose rigour on other fields and to encounter new challenges that inspire new theoretical developments.

His friends' and colleagues' testimony that he tries to keep the highest ethical and scientific standards in his research and in his dealings with colleagues, students, and other people around him. New students are treated with the same courtesy as leading researchers. This is reflected in the fact that many former students continue to collaborate when they become more senior researchers.

He is remarkably generous in sharing and discussing the many ideas emanating from his fertile mind, and is genuinely curious and appreciative of other opinions. This collaborative spirit is also witnessed by him having 132 coauthors listed on DBLP. Despite being one of our generation’s leading computer scientists, many of his collaborators first and foremost consider him to be a remarkably loyal and true friend.

He was inducted as an ACM Fellow in 2020 "for the development of logical methods for design and verification of computational systems".^[6][7]

Selected research

• Clavel, Manuel, et al. All about Maude — a high-performance logical framework: how to specify, program and verify systems in rewriting logic. Springer-Verlag, 2007.
• Goguen, Joseph A., et al. "Introducing obj." Software Engineering with OBJ. Springer, Boston, MA, 2000. 3–167.
• Meseguer, José. "Conditional rewriting logic as a unified model of concurrency." Theoretical computer science 96.1 (1992): 73–155.
• Goguen, Joseph A., and José Meseguer. "Security policies and security models." 1982 IEEE Symposium on Security and Privacy. IEEE, 1982.