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
 

Mahyar Karimi photo
Mahyar Karimi
PhD Student

Mahyar.Karimi@ist.ac.at
 

Konstantin Kueffner photo
Konstantin Kueffner
PhD Student

konstantin.kueffner@ista.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
 

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

Thejaswini.k.s@ist.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

Chalupa M, Henzinger TA, Oliveira da Costa A. Monitoring extended hypernode logic. In: Integrated Formal Methods. Vol 15234. Springer Nature; 2024:151-171. doi:10.1007/978-3-031-76554-4_9
Henzinger TA. Reminiscences of a Real-Time Researcher. In: Graf S, Pettersson P, Steffen B, eds. Real Time and Such. 15230. Cham: Springer Nature Switzerland; 2024:154-164. doi:10.1007/978-3-031-73751-0_12
Bonakdarpour B, Momtaz A, Nickovic D, Sarac NE. Approximate distributed monitoring under partial synchrony: Balancing speed & accuracy. In: 24th International Conference on Runtime Verification. Vol 15191. Springer Nature; 2024:282-301. doi:10.1007/978-3-031-74234-7_18
Bose S, Henzinger TA, Lehtinen K, Schewe S, Totzke P. History-deterministic timed automata. Logical Methods in Computer Science. 2024;20(4):1-28. doi:10.46298/lmcs-20(4:1)2024
Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. VAMOS: Middleware for best-effort third-party monitoring. Science of Computer Programming. 2024;240. doi:10.1016/j.scico.2024.103212
Beneš N, Brim L, Huvar O, Pastva S, Šafránek D. BNClassifier: Classifying boolean models by dynamic properties. In: Computational Methods in Systems Biology. Vol 14971. Springer Nature; 2024:19-26. doi:10.1007/978-3-031-71671-3_2
Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. QuAK: Quantitative Automata Kit. arXiv. doi:10.48550/arXiv.2409.03569
Avni G, Goharshady EK, Henzinger TA, Mallik K. Bidding games with charging. In: 35th International Conference on Concurrency Theory. Vol 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2024. doi:10.4230/LIPIcs.CONCUR.2024.8
Boker U, Henzinger TA, Lehtinen K, Prakash A. History-determinism vs fair simulation. In: 35th International Conference on Concurrency Theory. Vol 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2024. doi:10.4230/LIPIcs.CONCUR.2024.12
Henzinger TA, Mazzocchi NA, Sarac NE. Strategic dominance: A new preorder for nondeterministic processes. In: 35th International Conference on Concurrency Theory. Vol 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2024. doi:10.4230/LIPIcs.CONCUR.2024.29

Current projects