Moshe Y Vardi

Moshe Vardi has made major contributions to a wide variety of fields, including database theory, program verification, finite model theory, reasoning about knowledge, and constraint satisfaction. He is perhaps the most influential researcher working at the interface of logic and computer science, building bridges between communities in computer science and beyond. With his collaborators he has made fundamental contributions to major research areas, including: 1) Investigation of the logical theory of databases, where his focus on the trade-off between expressiveness and computational complexity laid the foundations for work on integrity constraints, complexity of query evaluation, incomplete information, database updates, and logic programming in databases. 2) The automata-theoretic approach to reactive systems, which laid mathematical foundations for verifying that a program meets its specifications. 3) Reasoning about knowledge through his development of epistemic logic.

In database theory, Vardi developed a theory of general data dependencies, finding axiomatizations and resolving their decision problem; introduced two basic notions of measuring the complexity of algorithms for evaluating queries, data-complexity and query-complexity, which soon became standard in the field; created a logical theory of data updates; and characterized the expressive power of query languages and related them to complexity classes. In software and hardware verification, Vardi introduced an automata-theoretic approach to the verification of reactive systems that revolutionized the field, using automata on infinite strings and trees to represent both the system being analyzed and undesirable computations of the system. Vardi's automata-theoretic approach has played a central role over the last 30 years of research in the field and in the development of verification tools. In constraint satisfaction, the Feder-Vardi Dichotomy Conjecture has generated decades of research, especially among algebraists who went on to develop a profound connection between the complexity of constraint satisfaction and universal algebra. In knowledge theory, Vardi developed rigorous foundations for reasoning about the knowledge of multi-agent and distributed systems, a problem of central importance in many disciplines; his co-authored book on the subject is the definitive source for this field.

From the moment the first issue appeared under his editorship (July 2008), it was clear Communications of the ACM had been transformed on all fronts: full of industry news, insightful and biting commentary, stories of real-world applications, historic technology overviews, and in-depth computing research digestible to a broad-based audience. This was a Communications worthy of ACM's membership because it offered a truly global view of the computing community. Over the last 10 years, Moshe has made it his mission to keep Communications at the forefront of computing coverage, insisting content be of the highest quality and including voices from all disciplines. He also succeeded in making the content accessible from anywhere in the world. Over the last several years, a website, digital edition, and mobile apps have made Communications available from anywhere and on any device.

In June, 2017, Moshe stepped down as editor-in-chief of Communications. For his exhaustive dedication and commitment to editorial excellence, we honor him with the ACM Presidential Award.

Revitalization of Communications of the ACM (CACM)

In late 2006 Moshe Y. Vardi took on the task of revitalizing and redefining Communications of the ACM. His goal was to create a publication that reflected the very best of computing research, education, and practice. His approach was influenced by Science, the weekly publication of AAAS, which covers research, practice, news, and opinion for the broad scientific community. As Editor-in-Chief of Communications, Vardi added compelling features including viewpoints, practice, and research highlights, enabling the activity, contributions and insights of computing to be communicated through a variety of perspectives and contexts. He assembled a number of outstanding editorial board sections, each populated with distinguished computing professionals, and each focused on a specific area of the magazine: research highlights, practice, contributed and review articles, news and viewpoints.

Communications, through Vardi's efforts, is now a publication of interest to practitioners, researchers, educators, and the educated public alike. The result is truly a flagship publication of ACM, and an effective communication vehicle for our discipline to the world at large.

Outsourcing Study

In early 2004 the issue of outsourcing and job migration was increasingly a concern to the computing community. There were questions as to what was really going on: Were jobs actually moving? Was there no future for IT professionals? What would be the long-term impact on academic/research communities?

Funded by the ACM Council, and with the help of Frank Mayadas and William Aspray, Vardi assembled a 30-person international task force to look at the issue. In a yearlong effort, he guided the task force in a systematic, scientific analysis of the forces underpinning job migration. The result of this analysis was a widely-circulated report, Globalization and Offshoring of Software, which was released in February 2006.

Vardi has helped lay the foundation for arguments that the entire computing field has embraced: that the world of computing is globalizing, that investment in computing research is fundamentally important to innovation, that the study of computer science is critical to competitive 21st century skill sets, and that strong educational systems in which computation plays a fundamental role will be defining success measures in a competitive global economy.

A key problem in computer science is finding ways to verify that hardware and software designs meet their specifications. This problem is particularly acute in reactive systems, which are systems that interact with their environments, such as digital systems and communication protocols. The four awardees demonstrated that checking the correctness of reactive systems can be done based on a mathematical analysis of automata. Specifically, questions about correctness of reactive systems with respect to expressive specifications can be reduced to questions about finite automata on infinitary input structures. They showed how this approach enables the development of algorithms that could be made efficient enough to automate reasoning in practice. Carrying out the automata-theoretic approach required advances in both automata theory and the theory of program logics. This connection brought a wealth of new techniques to the theory of program logics, and the new application revived the theory of automata on infinitary inputs. Their body of work provided the algorithmic foundations for many formal-verification tools. Furthermore, they were personally involved in the development of industrial verification tools via technology transfer and the development of the verification systems COSPAN and SPIN. Their techniques are widely used commercially in the development of "control-intensive" software programs.