Tom Henzinger Group

Tom Henzinger’s group is interested in mathematical methods for improving the quality of software. More and more aspects of our lives are controlled by software and over 90% of the computing power is in places you wouldn’t expect, such as cell phones, kitchen appliances, and pacemakers. Computer software has, at the same time, become one of the most complicated artifacts produced by man. It is therefore unavoidable that software contains errors and vulnerabilities, and preventing and fixing software bugs is a major technological challenge.

List of research topics includes:

  • Analysis and synthesis of concurrent software
  • Quantitative modeling and verification of reactive systems
  • Predictability and robustness for real-time and embedded systems
  • Model checking biochemical reaction networks
  • Formal methods for neural networks
  • Formal methods for quantum computation
  • Run-time verification

If you are interested in pursuing a doctoral degree or postdoc in our group, please contact us. The application procedure for graduate students is described at the PhD admission page.

Current group members

Marek Chalupa photo
Marek Chalupa
Postdoc

marek.chalupa@ista.ac.at
 

Thejaswini K. S. photo
Thejaswini K. S.
Postdoc

Thejaswini.k.s@ist.ac.at
 

Konstantin Kueffner photo
Konstantin Kueffner
PhD Student

konstantin.kueffner@ista.ac.at
 

Kaushik Mallik photo
Kaushik Mallik
Postdoc

Kaushik.Mallik@ist.ac.at
 

Stefanie Muroya Lei photo
Stefanie Muroya Lei
PhD Student

Stefanie.MuroyaLei@ist.ac.at
 

Ana Oliveira da Costa photo
Ana Oliveira da Costa
Postdoc

ana.costa@ista.ac.at
 

Samuel Pastva photo
Samuel Pastva
ISTA Fellow

samuel.pastva@ista.ac.at
 

Zhengqi Yu photo
Zhengqi Yu
Postdoc

Zhengqi.Yu@ist.ac.at
 

Past group members

PhD students
Interns
  • Ouldouz Neysari (2023 )
  • Stefanie Muroya Lei (2022 )
  • Pavol Kebis (2022 )
  • Mahyar Karimi (2022 )
  • Parand Alizadeh Alamdari (2019 )
  • Soroush Ebadian (2019 )
  • Milad Aghajohari (2018 )
  • Alexander Scharinger (2018 )
  • N. Ege Sarac (2017 )
  • Bharat Khandelwal (2017 )
  • Chris Wendler (2016 )
  • Shubham Goel (2016 )
  • Aviral Kumar (2016 )
  • Charmi Dedhia (2015 )
  • Pradyot Prakash (2015 )
  • Pratik Pramod Fegade (2014 )
  • Vansh Pahwa (2014 )
  • Matthias Loening (2013 )
  • Sameep Bagadia (2013 )
  • Alexandre Thevenet-Montagne (2012 )
  • Aditya Ayyar (2012 )
  • Vipul Singh (2012 )
  • Gopi Sivakanth (2011 )
  • Nishant Totla (2010, 2011 )
  • Rohit Singh (2010 )
  • Raluca Halalai (2010 )
  • Yashdeep Godhal (2010 )
Administrative Assistant
Ksenja Harpprecht
ksenja.harpprecht@ist.ac.at
+43 2243 9000 1015
Am Campus 1, A-3400 Klosterneuburg

Courses

Formalisms Every Computer Scientist Should Know
Tuesdays 8:45-10:00 C_CS-3002_F23

We will talk about logics, automata, grammars, function calculi, and process calculi, with an emphasis on syntax, operational semantics, and denotational semantics. We will also learn how to write definitions and proofs at different levels of formality.

Seminars and events

Recent publications

Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Oliveira da Costa A. Information-flow interfaces. Formal Methods in System Design. 2024. doi:10.1007/s10703-024-00447-0
Majumdar R, Sağlam I, Thejaswini KS. Rabin games and colourful universal trees. In: 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Vol 14572. Springer Nature; 2024:213-231. doi:10.1007/978-3-031-57256-2_11
Chalupa M, Richter C. Bubaak-SpLit: Split what you cannot verify (Competition contribution). In: 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Vol 14572. Springer Nature; 2024:353–358. doi:10.1007/978-3-031-57256-2_20
Avni G, Mallik K, Sadhukhan S. Auction-based scheduling. In: 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Vol 14572. Springer Nature; 2024:153-172. doi:10.1007/978-3-031-57256-2_8
Trinh G, Benhamou B, Pastva S, Soliman S. Scalable enumeration of trap spaces in boolean networks via answer set programming. In: Proceedings of the 38th AAAI Conference on Artificial Intelligence. Vol 38. Association for the Advancement of Artificial Intelligence; 2024:10714-10722. doi:10.1609/aaai.v38i9.28943
Froleyks N, Yu Z, Biere A. Ternary simulation as abstract interpretation (Work in Progress). In: 27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems. ; :148-151.

Current projects