Thomas A. Henzinger
Institute of Science and Technology Austria
|
Primary Section: 34, Computer and Information Sciences Membership Type:
Member
(elected 2020)
|
Biosketch
Tom Henzinger has been President of IST Austria (Institute of Science and Technology Austria) since 2009. He holds a Dipl.-Ing. degree in Computer Science from Johannes Kepler University in Linz, Austria, an M.S. degree in Computer and Information Sciences from the University of Delaware, a Ph.D. degree in Computer Science from Stanford University (1991), and Dr.h.c. degrees from Fourier University in Grenoble, France, and from Masaryk University in Brno, Czech Republic. He was Assistant Professor of Computer Science at Cornell University and Professor of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He was also Director at the Max-Planck Institute for Computer Science in Saarbrucken, Germany, and Professor of Computer and Communication Sciences at EPFL in Lausanne, Switzerland. His research focuses on the theory of software systems, especially models, algorithms, and tools for the design and verification of reliable software. His HyTech tool was the first model checker for mixed discrete-continuous systems. He is a member of the US National Academy of Sciences, the American Academy of Arts and Sciences, Academia Europaea, the German Academy of Sciences (Leopoldina), and the Austrian Academy of Sciences. He is also a Fellow of the AAAS, the ACM, and the IEEE. He has received the Robin Milner Award of the Royal Society, the EATCS Award of the European Association for Theoretical Computer Science, and the Wittgenstein Award of the Austrian Science Fund.
Research Interests
Tom Henzinger builds formal modeling languages and algorithmic software tools for the design and verification of reliable computerized systems. Software is particularly error-prone and difficult to debug if many components of a system act and interact concurrently, and if the requirements on the system demand a response in real time. The design of such software needs to be based on rigorous engineering principles derived from symbolic logic and formal models of computation. Tom and his collaborators developed the model of hybrid automata for the algorithmic analysis of mixed discrete-continuous systems; real-time temporal logic, alternating-time temporal logic, and strategy logic for the automated reasoning about multi-agent systems; the specification languages of reactive modules and interface automata for the disciplined construction of safe multi-component systems; time-triggered programming and embedded machine code for the implementation of predictable real-time systems; and software tools for system analysis based on the automatic goal-directed (“lazy”) refinement of formal abstractions. His current interests focus on solving concurrent and bidding graph games for the algorithmic synthesis of control systems; on defining and checking quantitative correctness and robustness measures for software; on developing formal methods for increasing the trust in machine-learned systems; and on designing executable symbolic models for biological systems.
