The EATCS has just announced that

Thomas Henzinger is the

EATCS Award 2019 recipient for "fundamental contributions to the theory and practice of formal verification and synthesis of reactive, real-time, and hybrid computer systems, and to the application of formal methods to biological systems." Congratulations to the award committee---consisting of Artur Czumaj, Marta Kwiatkowska and Christos Papadimitriou (chair)---for their great choice, to Tom for a very well deserved award and to the TCS community at large.

Of course, Tom Henzinger needs no introduction. However, let me use this post to provide a bird's eye view of his career and of some of his many contributions to TCS, which would be enough for a good number of very successful research careers. The text below is largely due to

Jean-Francois Raskin.

**Biographical sketch**
Thomas A. Henzinger is the President of

IST Austria (Institute of Science and Technology Austria), which, under his leadership, has quickly become one of the most impactful research institutes in the world. Before joining IST as its first president, Tom was Assistant Professor of Computer Science at Cornell
University (1992-95), Assistant Professor (1996-97), Associate Professor (1997-98) and Professor
(1998-2004) of Electrical Engineering and Computer Sciences at the University of California, Berkeley.
He was also the Director of the Max-Planck Institute for Computer Science in Saarbruecken, Germany
(1999) and Professor of Computer and Communication Sciences at EPFL in Lausanne, Switzerland
(2004-09).

Tom is an ISI highly cited researcher and his h-index is 103, according to

Google Scholar. He is a member of Academia
Europaea, a member of the German Academy of Sciences (Leopoldina), a member of the Austrian
Academy of Sciences, a Fellow of the AAAS, a Fellow of the EATCS, a Fellow of the ACM, and a Fellow
of the IEEE. He was the recipient of the
Milner Award of the Royal Society in 2015, of the Wittgenstein Award of the Austrian Science Fund and was granted an ERC Advanced Investigator Grant in 2010. He received the SIGPLAN POPL Most
Influential Paper Award (2014), Logic in Computer Science Test-of-Time Award (2012), ACM SIGSOFT
Impact Paper Award (2011), and Best Paper awards at SIGSOFT FSE and CONCUR.

**Main scientific achievements** Tom's research focuses on modern systems theory, especially models, algorithms, and tools for the
design and verification of reliable software, hardware and embedded systems. His

HyTech tool was
the first model checker for mixed discrete-continuous systems.

Tom has made a large number of fundamental contributions to theoretical computer
science. Here I will limit myself to mentioning a small number of research areas where he has been particularly prolific and
influential.

*The theory of timed and hybrid systems.* Tom has defined and studied the expressiveness and the
algorithmic complexity of several real-time extensions of temporal logics. He is one of the most
important contributors to the theory of hybrid automata and to algorithms for the analysis of suchmodels. His papers on the subject are among the most cited ones in the field of computer-aided verification. As an example, his paper “Symbolic model checking for real-time systems” received a LICS
Test-of-Time Award in 2012. He has also studied the gap that exists between mathematical
models of systems (e.g. hybrid automata) and their implementation on physical hardware. To bridge
this gap, he developed models of physical platforms such as Giotto and E-machines, and he devised
ways to relate their semantics with the one of the abstract mathematical models.
*Games for verification and control.* Tom has introduced the logic ATL*, which extends LTL and CTL* with
the ability to reason about strategies that can be played by coalitions of agents/components in models
of multi-agent/component systems. He has contributed to the understanding of the potential of
adopting concepts from game theory for modeling and reasoning about open systems. He has
contributed to a large number of algorithmic advances for solving game-graph problems and to better
understand their computational complexity.
*From Boolean models to quantitative models for verification and synthesis.* Tom has recently
investigated how to shift from Boolean models to quantitative models. This research proposes
quantitative generalizations of the paradigms that had success in reactive modeling, such as
compositionality, property-preserving abstraction, model checking and synthesis. With those models,
we can specify and reason about quantitative aspects, such as resource consumption, or compare the
performance of different design solutions in embedded systems. He has obtained a substantial
funding from the European Research Council to proceed along this promising line of research.
*Foundations of software model checking.* Tom has contributed substantially to the algorithms
underlying the analysis of software systems by introducing the concept of lazy abstraction. Those
ideas have been implemented in the highly influential tool Blast. This line of work was honoured with the
Most Influential 2004 POPL Paper Award which he received in 2014.
*Computational modelling of biological systems.* Tom and his coworkers have shown that computational models are well
suited to model the dynamics of biological systems. This is part of a broader research program that
has the objective to show that concepts introduced to formalize reactive systems are helpful to model
and reason about biological systems.

Those important theoretical contributions have always been developed with relevant practical
applications in mind. Consequently, Thomas Henzinger has not only worked on the foundations of our subject, but
he also transferred his theoretical ideas into practice by developing tools and by suggesting
methodologies that could be used in applying his theoretical results.

Tom is a research leader who has had a profound influence on his PhD students and
post-docs. To wit, several of his former students are now well-recognized researchers that enrich the life of
our research community and now lead successful research groups.

**Addendum 12 April 2019:** In case you are interested, you can find a short interview I had with Tom Henzinger a while back

here.