USA - 2009
For outstanding leadership in restructuring the Communications of the ACM to be the flagship publication of both the Association and the discipline and in organizing an influential, systematic analysis of outsourcing.
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.
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.
USA - 2008
For his unwavering commitment in driving the ACM Job Migration Task Force and its Globalization and Offshoring of Software report, drawing worldwide attention to its wealth of information and balanced perspective. Dr. Vardi's ambitious efforts on behalf of ACM continue as he energetically leads the revitalization of ACM's flagship publication, Communications of the ACM, and becomes its new editor-in-chief.
USA - 2005
Gerard J. Holzmann, Robert P. Kurshan, Moshe Y. Vardi, Pierre Wolper
For the development of automata-theoretic techniques for reactive-systems verification, and the practical realization of powerful formal-verification tools based on these techniques.
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.
USA - 2000
For contributions to the development of logic as a unifying foundational framework and a tool for modeling computational systems.