Prof. José Meseguer, professor of computer science at University of Illinois, Urbana-Champaign (USA), has been awarded the FME Fellowship 2019. The Fellowships are awarded every three years in recognition of technical breakthroughs and pioneering work in advancing, applying, and promoting mathematically rigorous methods for the design of computing systems.
Prof. José Meseguer receives the FME 2019 Fellowship.
The call for nominations was issued in October 2018, and on 15 December 2018 this process was concluded. In a ceremony at the 3rd World Congress on Formal Methods (FM 2019) Prof. Meseguer was announced as being the third Fellow of Formal Methods Europe. After Prof. Ana Cavalcanti, the Chair of FME, introduced the new FME Fellow and explained the selection process, Prof. José Meseguer shared his insights in a talk with the title “Designing Systems in Rewriting Logic: The Power of the Thought Experiment” about his work and scientific achievements. At the end of the ceremony, Prof. Meseguer was presented with a certificate and medal.
Prof. José Meseguer during his FME
2019 Fellowship lecture
"Designing Systems in Rewriting
Logic: The Power of the Thought Experiment".
The FME Awards Committee motivated its decision as follows:
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 is 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.