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.
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.
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.
Regular group seminar held each Tuesday at ISTA.
A joint seminar with FORSYTE group at TU Wien.
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 |