The EATCS Award 2012 - Laudatio for Moshe Vardi

The EATCS Awards Committee consisting of Leslie Ann Goldberg, Friedhelm Meyer auf der Heide and Eugenio Moggi (chair), has unanimously decided to give the EATCS Award to Professor Moshe Vardi. (pdf)

Moshe Vardi is an extremely active and productive researcher. His work so far has been very inuential, certainly in science, but also in dissemination and policy matters. We are pleased to recognise these contributions with an EATCS Award.

Research Contributions
Vardi has made fundamental and lasting research contributions to the development of mathematical logic as a unifying foundational framework for modeling computational systems. His research has focused on applying and developing logic in computing, and has played a major role in our present understanding and use of logic in computing. Vardi has contributed to several areas of Computer Science, in particular: software and hardware verification;
databases; complexity theory; and distributed systems.

Automata-theoretic approach to design verication.

Vardi has demonstrated that questions about correctness of hardware and software designs can be reduced to algorithmic questions about nite automata on innitary input structures (innite words or innite trees). Carrying out this 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 innitary inputs.

His 1986 paper, "An automata-theoretic approach to automatic program verification", has over 1350 citations, it won an IBM Outstanding Innovation Award in 1989, an ACM-EATCS Goedel Prize in 2000, a LICS Test-of-Time Award in 2006, and an ACM Kanellakis Award for Theory and Practice in 2006.

This line of work is the basis of several academic and industrial automated verification tools, such as the model checker SPIN that won the 2001 ACM's Software System award. The work has also inuenced emerging specification languages, such as the IEEE Standard Property Specication Language (PSL) for writing requirements of hardware designs, and the manner in which specifications are checked by industrial model checkers.

Theory of database queries. Database management systems have evolved
from unsophisticated databases, which are essentially structured collections
of data, toward smart databases possessing deductive capabilities. Vardi has investigated the theory of database queries, with a focus on the trade-off between expressiveness and computational complexity. His research
laid the foundations in the following areas: integrity constraints, complexity of query evaluation, querying incomplete information, database updates, universal-relation interfaces, and database logic programming.
In his 1982 paper "The complexity of relational query languages", Vardi showed that there are two fundamentally different ways to measure the complexity of queries, referred to as data complexity and expression complexity, a classification that is today widely accepted. This paper has over 1150 citations.
His 1998 paper, Conjunctive-query containment and constraint satisfaction, which exhibited a deep connection between conjunctive-query evaluation and constraint-satisfaction solving, received an ACM PODS Mendelzon Test-of-Time Award in 2008. In 2008 Vardi received the ACM Edgar F. Codd Innovations Award, the top recognition for database research accomplishments.

Descriptive complexity theory. Computational Complexity focuses on classifying computational problems according to their inherent difficulty in terms of resource (such as time or space) requirements.
Descriptive complexity theory is a branch of computational complexity theory that characterizes complexity classes by the type of logic needed to express them. An example is a classical result, proved by Vardi (and independently by Immerman) in 1982, that characterizes the complexity class PTIME is terms of rst-order logic enriched with the xpoint operator. (This work won an IBM Outstanding Innovation Award in 1992.)
His 1993 paper, Monotone monadic SNP and constraint satisfaction, used logic, graph theory, and algebra, to study the computational complexity of constraint-satisfaction problems. The 1998 paper, The computational structure of monotone monadic SNP and constraint satisfaction: a study through Datalog and group theory, has more than 500 citations. Together, these papers form the basis for work on the complexity of constraint satisfaction.

Knowledge in multi-agent systems.

Reasoning about knowledge has applications in such diverse elds as economics, linguistics, artificial intelligence and computer science. In a distributed system a process may need to know
whether other processes know that a message has been lost.

Together with his collaborators, Vardi developed an extensive theory of reasoning about knowledge. This work focuses on using reasoning about knowledge to design, analyze and verify the correctness of multi-agent systems.
The work provides good formal models of knowledge that are appropriate for multiple applications. This work won an IBM Outstanding Innovation Award in 1987. The book entitled Reasoning about Knowledge by Fagin, Moses, Halpern and Vardi, rst published by MIT Press in 1995, is now considered a classic, with over 2900 citations.
In additional to fundamental contributions, Vardi also shaped the eld by pointing out promising research directions.

Scientic Dissemination and Impact
Vardi's scientic output is impressive and very inuential.

• He is author or co-author of over 400 publications, including 2 books:
• Reasoning about Knowledge and Finite Model Theory and its Applications.
• He has more than 20000 citations and an h-index above 75.
• He has a huge number of collaborations, e.g. on publications he has almost 200 co-authors.

Leadership and Service
Vardi has a long service record and a strong leadership in the eld, in par-
ticular:

• He has played a central role in the IEEE Symposium on Logic in Computer Science (LICS), for which he served as General Chair for several years, and he has been the major force behind the creation of the Federated Logic Conferences (FLoC).
• As Editor-in-Chief, he has performed admirably in rethinking and leading Communications of the ACM. This service to the whole community is commendable in its own right, but his vision led to important changes, like the introduction of the excellent new section on research highlights.

Conclusions.
For all the above reasons, the EATCS awards Committee
unanimously decided to give the EATCS award to Professor Moshe Vardi.

The EATCS awards Committee 2012
Leslie Ann Goldberg
Friedhelm Meyer auf der Heide
Eugenio Moggi (chair)