The EATCS Award 2025  - Laudation for Rajeev Alur

The EATCS Award committee selects as the recipient of the 2025 EATCS Award for his contributions to computer-assisted specification, analysis, verification, and synthesis of systems. Alur's research is characterized by deep and elegant theoretical ideas with a clear path to practical industrial use. His multiple celebrated contributions include the following:

During the 1990s, in collaboration with Dill, Henzinger, and others, Rajeev Alur introduced and studied timed and hybrid automata. These models have since been further explored in thousands of articles, and the resulting analysis and verification algorithms have been implemented in numerous tools.

In the late 1990s and early 2000s, Alur, together with Henzinger and Kupferman, introduced alternating-time temporal logic, a logical foundation for multi-agent and strategic reasoning in reactive systems. This work influenced fields beyond formal verification, such as control theory and AI planning.

In the 2000s, Alur studied formalisms for modeling and specifying structured programs. In collaboration with Madhusudan, he demonstrated that many verification problems for such programs reduce to questions on nested word automata (also known as visibly pushdown automata), leading to novel verification algorithms.

Since the mid-2010s, Alur has made fundamental contributions to computer-assisted synthesis of correct-by-construction program fragments. Along with his collaborators, he introduced syntax-guided synthesis (SyGuS), a framework that combines symbolic constraint solving with syntax-guided heuristic search.

Summarizing, Rajeev Alur's contributions have transformed the field of formal methods and played a crucial role in establishing cyber-physical systems as an academic discipline.