ABOUT NEWS PEOPLE RESEARCH COURSES JOBS
Research
Formal Methods in Security and Privacy

Using formal methods we are able to provide strong mathematical guarantees for security and privacy. This can be achieved through manual proofs, or automated techniques such as model checking or type systems. Formal methods can be applied to all areas of security and privacy research.

PEOPLE
Krishnendu Chatterjee
Krishnendu Chatterjee
Professor (IST Austria) ↗
Thomas Henzinger
Thomas Henzinger
Professor (IST Austria) ↗
Laura Kovács
Laura Kovács
Professor (TU Wien) ↗
Matteo Maffei
Matteo Maffei
Professor (TU Wien) ↗
PUBLICATIONS

A Quantitative Analysis of Security, Anonymity and Scalability for the Lightning Network. Sergei Tikhomirov, Pedro Moreno-Sanchez, Matteo Maffei (eprint)
A Survey of Bidding Games on Graphs (Invited Paper). Guy Avni, Thomas A. Henzinger (CONCUR)
Algebra-based Loop Synthesis. Andreas Humenberger, Laura Kovács (eprint)
Analysis of Bayesian Networks via Prob-Solvable Loops. Ezio Bartocci, Laura Kovács, Miroslav Stankovic (eprint)
Approximating Values of Generalized-Reachability Stochastic Games. Pranav Ashok, Krishnendu Chatterjee, Jan Kretínský, Maximilian Weininger, Tobias Winkler (LICS)
Concentration-Bound Analysis for Probabilistic Programs and Probabilistic Recurrence Relations. Jinyi Wang, Yican Sun, Hongfei Fu, Mingzhang Huang, Amir Kafshdar Goharshady, Krishnendu Chatterjee (eprint)
Dynamic resource allocation games. Guy Avni, Thomas A. Henzinger, Orna Kupferman (Theor. Comput. Sci.)
Faster Algorithms for Quantitative Analysis of Markov Chains and Markov Decision Processes with Small Treewidth. Ali Asadi, Krishnendu Chatterjee, Amir Kafshdar Goharshady, Kiarash Mohammadi, Andreas Pavlogiannis (eprint)
Formal Methods with a Touch of Magic. Parand Alizadeh Alamdari, Guy Avni, Thomas A. Henzinger, Anna Lukina (eprint)
Formalizing Graph Trail Properties in Isabelle/HOL. Laura Kovács, Hanna Lachnitt, Stefan Szeider (CICM)
How Many Bits Does it Take to Quantize Your Neural Network? Mirco Giacobbe, Thomas A. Henzinger, Mathias Lechner (TACAS)
Induction with Generalization in Superposition Reasoning. Márton Hajdú, Petra Hozzová, Laura Kovács, Johannes Schoisswohl, Andrei Voronkov (CICM)
Inductive Reachability Witnesses. Ali Asadi, Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, Mohammad Mahdavi (eprint)
Inductive sequentialization of asynchronous programs. Bernhard Kragl, Constantin Enea, Thomas A. Henzinger, Suha Orhun Mutluergil, Shaz Qadeer (PLDI)
Information-Flow Interfaces. Ezio Bartocci, Thomas Ferrère, Thomas A. Henzinger, Dejan Nickovic, Ana Oliveira da Costa (eprint)
Interactive Visualization of Saturation Attempts in Vampire. Bernhard Gleiss, Laura Kovács, Lena Schnedlitz (eprint)
Language-Based Web Session Integrity. Stefano Calzavara, Riccardo Focardi, Niklas Grimm, Matteo Maffei, Mauro Tempesta (CSF)
Language-Based Web Session Integrity. Stefano Calzavara, Riccardo Focardi, Niklas Grimm, Matteo Maffei, Mauro Tempesta (eprint)
Limits on amplifiers of natural selection under death-Birth updating. Josef Tkadlec, Andreas Pavlogiannis, Krishnendu Chatterjee, Martin A. Nowak (PLoS Computational Biology)
Monitoring Event Frequencies. Thomas Ferrère, Thomas A. Henzinger, Bernhard Kragl (CSL)
Mora - Automatic Generation of Moment-Based Invariants. Ezio Bartocci, Laura Kovács, Miroslav Stankovic (TACAS)
Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States. Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop (CONCUR)
Multi-dimensional Long-Run Average Problems for Vector Addition Systems with States. Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop (eprint)
Multiple-Environment Markov Decision Processes - Efficient Analysis and Applications. Krishnendu Chatterjee, Martin Chmelík, Deep Karkhanis, Petr Novotný, Amélie Royer (ICAPS)
Optimal and Perfectly Parallel Algorithms for On-demand Data-Flow Analysis. Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, Andreas Pavlogiannis (ESOP)
Optimal and Perfectly Parallel Algorithms for On-demand Data-flow Analysis. Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, Andreas Pavlogiannis (eprint)
Polynomial invariant generation for non-deterministic recursive programs. Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady (PLDI)
Proving Almost-Sure Termination of Probabilistic Programs via Incremental Pruning. Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný, Jiri Zárevúcky, Dorde Zikelic (eprint)
Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time. Peixin Wang, Hongfei Fu, Krishnendu Chatterjee, Yuxin Deng, Ming Xu (Proc. ACM Program. Lang.)
Refinement for Structured Concurrent Programs. Bernhard Kragl, Shaz Qadeer, Thomas A. Henzinger (CAV)
Reinforcement Learning of Risk-Constrained Policies in Markov Decision Processes. Tomás Brázdil, Krishnendu Chatterjee, Petr Novotný, Jiri Vahala (AAAI)
Reinforcement Learning of Risk-Constrained Policies in Markov Decision Processes. Tomás Brázdil, Krishnendu Chatterjee, Petr Novotný, Jiri Vahala (eprint)
Simplified Game of Life - Algorithms and Complexity. Krishnendu Chatterjee, Rasmus Ibsen-Jensen, Ismaël Jecker, Jakub Svoboda (MFCS)
Stochastic Games with Lexicographic Reachability-Safety Objectives. Krishnendu Chatterjee, Joost-Pieter Katoen, Maximilian Weininger, Tobias Winkler (CAV)
Stochastic Games with Lexicographic Reachability-Safety Objectives. Krishnendu Chatterjee, Joost-Pieter Katoen, Maximilian Weininger, Tobias Winkler (eprint)
Subsumption Demodulation in First-Order Theorem Proving. Bernhard Gleiss, Laura Kovács, Jakob Rath (IJCAR)
Subsumption Demodulation in First-Order Theorem Proving. Bernhard Gleiss, Laura Kovács, Jakob Rath (eprint)
Trace Logic for Inductive Loop Reasoning. Pamina Georgiou, Bernhard Gleiss, Laura Kovács (eprint)
eThor - Practical and Provably Sound Static Analysis of Ethereum Smart Contracts. Clara Schneidewind, Ilya Grishchenko, Markus Scherer, Matteo Maffei (eprint)
Deciding Fast Termination for Probabilistic VASS with Nondeterminism. Tomás Brázdil, Krishnendu Chatterjee, Antonín Kucera, Petr Novotný, Dominik Velan (eprint)
Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops. Ezio Bartocci, Laura Kovács, Miroslav Stankovic (ATVA)
Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops. Ezio Bartocci, Laura Kovács, Miroslav Stankovic (eprint)
Bidding Games on Markov Decision Processes. Guy Avni, Thomas A. Henzinger, Rasmus Ibsen-Jensen, Petr Novotný (RP)
Bidding Mechanisms in Graph Games. Guy Avni, Thomas A. Henzinger, Dorde Zikelic (MFCS)
Bidding Mechanisms in Graph Games. Guy Avni, Thomas A. Henzinger, Dorde Zikelic (eprint)
Combinations of Qualitative Winning for Stochastic Parity Games. Krishnendu Chatterjee, Nir Piterman (CONCUR)
Compositional Analysis for Almost-Sure Termination of Probabilistic Programs. Mingzhang Huang, Hongfei Fu, Krishnendu Chatterjee, Amir Kafshdar Goharshady (eprint)
Compositional Specifications for ioco Testing. Przemyslaw Daca, Thomas A. Henzinger, Willibald Krenn, Dejan Nickovic (eprint)
Continuous-Time Models for System Design and Analysis. Rajeev Alur, Mirco Giacobbe, Thomas A. Henzinger, Kim G. Larsen, Marius Mikucionis (Computing and Software Science)
Cost Analysis of Nondeterministic Probabilistic Programs. Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, Peixin Wang, Xudong Qin, Wenjun Shi (eprint)
Cost analysis of nondeterministic probabilistic programs. Peixin Wang, Hongfei Fu, Amir Kafshdar Goharshady, Krishnendu Chatterjee, Xudong Qin, Wenjun Shi (PLDI)
Deciding Fast Termination for Probabilistic VASS with Nondeterminism. Tomás Brázdil, Krishnendu Chatterjee, Antonín Kucera, Petr Novotný, Dominik Velan (ATVA)
Determinacy in Discrete-Bidding Infinite-Duration Games. Milad Aghajohari, Guy Avni, Thomas A. Henzinger (CONCUR)
Determinacy in Discrete-Bidding Infinite-Duration Games. Milad Aghajohari, Guy Avni, Thomas A. Henzinger (eprint)
Efficient parameterized algorithms for data packing. Krishnendu Chatterjee, Amir Kafshdar Goharshady, Nastaran Okati, Andreas Pavlogiannis (Proc. ACM Program. Lang.)
Faster Algorithms for Dynamic Algebraic Queries in Basic RSMs with Constant Treewidth. Krishnendu Chatterjee, Amir Kafshdar Goharshady, Prateesh Goyal, Rasmus Ibsen-Jensen, Andreas Pavlogiannis (ACM Trans. Program. Lang. Syst.)
Graph Planning with Expected Finite Horizon. Krishnendu Chatterjee, Laurent Doyen (LICS)
Infinite-duration Bidding Games. Guy Avni, Thomas A. Henzinger, Ventsislav Chonev (J. ACM)
Interactive Visualization of Saturation Attempts in Vampire. Bernhard Gleiss, Laura Kovács, Lena Schnedlitz (IFM)
Lonely Points in Simplices. Maximilian Jaroschek, Manuel Kauers, Laura Kovács (eprint)
Long-Run Average Behavior of Vector Addition Systems with States. Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop (CONCUR)
Long-Run Average Behavior of Vector Addition Systems with States. Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop (eprint)
Membership-Based Synthesis of Linear Hybrid Automata. Miriam García Soto, Thomas A. Henzinger, Christian Schilling, Luka Zeleznik (CAV)
Modular verification for almost-sure termination of probabilistic programs. Mingzhang Huang, Hongfei Fu, Krishnendu Chatterjee, Amir Kafshdar Goharshady (Proc. ACM Program. Lang.)
Monitoring Event Frequencies. Thomas Ferrère, Thomas A. Henzinger, Bernhard Kragl (eprint)
Near-Linear Time Algorithms for Streett Objectives in Graphs and MDPs. Krishnendu Chatterjee, Wolfgang Dvorák, Monika Henzinger, Alexander Svozil (CONCUR)
Near-Linear Time Algorithms for Streett Objectives in Graphs and MDPs. Krishnendu Chatterjee, Wolfgang Dvorák, Monika Henzinger, Alexander Svozil (eprint)
Non-polynomial Worst-Case Analysis of Recursive Programs. Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady (ACM Trans. Program. Lang. Syst.)
Optimal Dyck Reachability for Data-Dependence and Alias Analysis. Krishnendu Chatterjee, Bhavya Choudhary, Andreas Pavlogiannis (eprint)
Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty. Hui Kong, Ezio Bartocci, Yu Jiang, Thomas A. Henzinger (FORMATS)
Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty. Hui Kong, Ezio Bartocci, Yu Jiang, Thomas A. Henzinger (eprint)
Polynomial Invariant Generation for Non-deterministic Recursive Programs. Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady (eprint)
Portfolio SAT and SMT Solving of Cardinality Constraints in Sensor Network Optimization. Gergely Kovásznai, Krisztián Gajdár, Laura Kovács (SYNASC)
Proving Expected Sensitivity of Probabilistic Programs with Randomized Execution Time. Peixin Wang, Hongfei Fu, Krishnendu Chatterjee, Kangli He, Ming Xu (eprint)
Quantitative Automata under Probabilistic Semantics. Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop (Log. Methods Comput. Sci.)
Quasipolynomial Set-Based Symbolic Algorithms for Parity Games. Krishnendu Chatterjee, Wolfgang Dvorák, Monika Henzinger, Alexander Svozil (eprint)
Run-Time Optimization for Learned Controllers Through Quantitative Games. Guy Avni, Roderick Bloem, Krishnendu Chatterjee, Thomas A. Henzinger, Bettina Könighofer, Stefan Pranger (CAV)
Strategy Representation by Decision Trees with Linear Classifiers. Pranav Ashok, Tomás Brázdil, Krishnendu Chatterjee, Jan Kretínský, Christoph H. Lampert, Viktor Toman (QEST)
Strategy Representation by Decision Trees with Linear Classifiers. Pranav Ashok, Tomás Brázdil, Krishnendu Chatterjee, Jan Kretínský, Christoph H. Lampert, Viktor Toman (eprint)
Superposition Reasoning about Quantified Bitvector Formulas. David Damestani, Laura Kovács, Martin Suda (SYNASC)
Termination of Nondeterministic Probabilistic Programs. Hongfei Fu, Krishnendu Chatterjee (VMCAI)
The Complexity of POMDPs with Long-run Average Objectives. Krishnendu Chatterjee, Raimundo Saona, Bruno Ziliotto (eprint)
The Evolutionary Price of Anarchy - Locally Bounded Agents in a Dynamic Virus Game. Laura Schmid, Krishnendu Chatterjee, Stefan Schmid (OPODIS)
The Evolutionary Price of Anarchy - Locally Bounded Agents in a Dynamic Virus Game. Krishnendu Chatterjee, Laura Schmid, Stefan Schmid (eprint)
The treewidth of smart contracts. Krishnendu Chatterjee, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady (SAC)
Transient Memory in Gene Regulation. Calin C. Guet, Thomas A. Henzinger, Claudia Igler, Tatjana Petrov, Ali Sezgin (CMSB)
Value-centric Dynamic Partial Order Reduction. Krishnendu Chatterjee, Andreas Pavlogiannis, Viktor Toman (eprint)
Value-centric dynamic partial order reduction. Krishnendu Chatterjee, Andreas Pavlogiannis, Viktor Toman (Proc. ACM Program. Lang.)
Verifying Relational Properties using Trace Logic. Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovács, Matteo Maffei (FMCAD)
Verifying Relational Properties using Trace Logic. Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovács, Matteo Maffei (eprint)
Members
Partners