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

Thejaswini K. S. photo
Thejaswini K. S.

Konstantin Kueffner photo
Konstantin Kueffner
PhD Student

Kaushik Mallik photo
Kaushik Mallik

Nicolas Mazzocchi photo
Nicolas Mazzocchi

Stefanie Muroya Lei photo
Stefanie Muroya Lei
PhD Student

Ana Oliveira da Costa photo
Ana Oliveira da Costa

Samuel Pastva photo
Samuel Pastva
ISTA Fellow

Zhengqi Yu photo
Zhengqi Yu

Past group members

PhD students
  • Parand Alizadeh Alamdari (Jul-Sep 2019 )
  • Soroush Ebadian (Jul-Sep 2019 )
  • Milad Aghajohari (Jul-Sep 2018 )
  • Alexander Scharinger (Jun-Aug 2018 )
  • N. Ege Sarac (Jun-Aug 2017 )
  • Bharat Khandelwal (May-Jul 2017 )
  • Chris Wendler (Jul-Aug 2016 )
  • Shubham Goel (May-Jul 2016 )
  • Aviral Kumar (May-Jul 2016 )
  • Charmi Dedhia (May-Jul 2015 )
  • Pradyot Prakash (May-Jul 2015 )
  • Pratik Pramod Fegade (Jun-Jul 2014 )
  • Vansh Pahwa (Jun-Jul 2014 )
  • Matthias Loening (Jul-Aug 2013 )
  • Sameep Bagadia (May-Jul 2013 )
  • Alexandre Thevenet-Montagne (Mar-Aug 2012 )
  • Aditya Ayyar (May-Jul 2012 )
  • Vipul Singh (May-Jul 2012 )
  • Gopi Sivakanth (May-Jul 2011 )
  • Nishant Totla (May-Jul 2010, May-Jul 2011 )
  • Rohit Singh (May-Jul 2010 )
Administrative Assistant
Ksenja Harpprecht
+43 2243 9000 1015
Am Campus 1, A-3400 Klosterneuburg


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

Majumdar R, Mallik K, Schmuck AK, Soudjani S. Symbolic control for stochastic systems via finite parity games. Nonlinear Analysis: Hybrid Systems. 2023;51. doi:10.1016/j.nahs.2023.101430
Beneš N, Brim L, Pastva S, Šafránek D, Šmijáková E. Phenotype control of partially specified boolean networks. In: International Conference on Computational Methods in Systems Biology. Vol 14137. Springer Nature; 2023:18-35. doi:10.1007/978-3-031-42697-1_2
Boker U, Henzinger TA, Mazzocchi NA, Sarac NE. Safety and liveness of quantitative automata. In: 34th International Conference on Concurrency Theory. Vol 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023. doi:10.4230/LIPIcs.CONCUR.2023.17
Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. Hypernode automata. In: 34th International Conference on Concurrency Theory. Vol 279. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023. doi:10.4230/LIPIcs.CONCUR.2023.21
Henzinger TA, Karimi M, Kueffner K, Mallik K. Monitoring algorithmic fairness. In: Computer Aided Verification. Vol 13965. Springer Nature; 2023:358–382. doi:10.1007/978-3-031-37703-7_17
Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. Regular methods for operator precedence languages. In: 50th International Colloquium on Automata, Languages, and Programming. Vol 261. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023:129:1–129:20. doi:10.4230/LIPIcs.ICALP.2023.129
Trinh VG, Benhamou B, Henzinger TA, Pastva S. Trap spaces of multi-valued networks: Definition, computation, and applications. Bioinformatics. 2023;39(Supplement_1):i513-i522. doi:10.1093/bioinformatics/btad262
Kueffner K, Lukina A, Schilling C, Henzinger TA. Into the unknown: Active monitoring of neural networks (extended version). International Journal on Software Tools for Technology Transfer. 2023. doi:10.1007/s10009-023-00711-4
Avni G, Jecker IR, Zikelic D. Bidding graph games with partially-observable budgets. In: Proceedings of the 37th AAAI Conference on Artificial Intelligence. Vol 37. ; 2023:5464-5471. doi:10.1609/aaai.v37i5.25679
Lechner M, Zikelic D, Chatterjee K, Henzinger TA, Rus D. Quantization-aware interval bound propagation for training certifiably robust quantized neural networks. In: Proceedings of the 37th AAAI Conference on Artificial Intelligence. Vol 37. Association for the Advancement of Artificial Intelligence; 2023:14964-14973. doi:10.1609/aaai.v37i12.26747

Current projects