Research
Formal Methods in Security and Privacy
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
PUBLICATIONS
A Deterministic Almost-Tight Distributed Algorithm for Approximating Single-Source Shortest Paths. Monika Henzinger, Sebastian Krinninger, Danupon Nanongkai (SIAM J. Comput., 2021) ↗
Algorithms and conditional lower bounds for planning problems. Krishnendu Chatterjee, Wolfgang Dvorák, Monika Henzinger, Alexander Svozil (Artif. Intell., 2021) ↗
Automated Generation of Exam Sheets for Automated Deduction. Petra Hozzová, Laura Kovács, Jakob Rath (CICM, 2021) ↗
Differentially Private Algorithms for Graphs Under Continual Observation. Hendrik Fichtenberger, Monika Henzinger, Wolfgang Ost (ESA, 2021) ↗
Dynamic Maintenance of Low-Stretch Probabilistic Tree Embeddings with Applications. Sebastian Forster, Gramoz Goranci, Monika Henzinger (SODA, 2021) ↗
Dynamic Set Cover - Improved Amortized and Worst-Case Update Time. Sayan Bhattacharya, Monika Henzinger, Danupon Nanongkai, Xiaowei Wu (SODA, 2021) ↗
Faster Algorithms for Bounded Liveness in Graphs and Game Graphs. Krishnendu Chatterjee, Monika Henzinger, Sagar Kale, Alexander Svozil (ICALP, 2021) ↗
Fully Dynamic k-Center Clustering in Low Dimensional Metrics. Gramoz Goranci, Monika Henzinger, Dariusz Leniowski, Christian Schulz, Alexander Svozil (ALENEX, 2021) ↗
Inductive Benchmarks for Automated Reasoning. Márton Hajdú, Petra Hozzová, Laura Kovács, Johannes Schoisswohl, Andrei Voronkov (CICM, 2021) ↗
Integer Induction in Saturation. Petra Hozzová, Laura Kovács, Andrei Voronkov (CADE, 2021) ↗
New Techniques and Fine-Grained Hardness for Dynamic Near-Additive Spanners. Thiago Bergamaschi, Monika Henzinger, Maximilian Probst Gutenberg, Virginia Vassilevska Williams, Nicole Wein (SODA, 2021) ↗
On Satisficing in Quantitative Games. Suguman Bansal, Krishnendu Chatterjee, Moshe Y. Vardi (TACAS, 2021) ↗
Optimal strategies for selecting coordinators. Martin Zeiner, Ulrich Schmid, Krishnendu Chatterjee (Discret. Appl. Math., 2021) ↗
Polynomial reachability witnesses via Stellensätze. Ali Asadi, Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, Mohammad Mahdavi (PLDI, 2021) ↗
Proving non-termination by program reversal. Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný, Dorde Zikelic (PLDI, 2021) ↗
Quantitative analysis of assertion violations in probabilistic programs. Jinyi Wang, Yican Sun, Hongfei Fu, Krishnendu Chatterjee, Amir Kafshdar Goharshady (PLDI, 2021) ↗
Quantitative and Approximate Monitoring. Thomas A. Henzinger, N. Ege Saraç (LICS, 2021) ↗
Solving Partially Observable Stochastic Shortest-Path Games. Petr Tomásek, Karel Horák, Aditya Aradhye, Branislav Bosanský, Krishnendu Chatterjee (IJCAI, 2021) ↗
Stateless Model Checking Under a Reads-Value-From Equivalence. Pratyush Agarwal, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis, Viktor Toman (CAV, 2021) ↗
Stochastic Processes with Expected Stopping Time. Krishnendu Chatterjee, Laurent Doyen (LICS, 2021) ↗
Symbolic Time and Space Tradeoffs for Probabilistic Verification. Krishnendu Chatterjee, Wolfgang Dvorák, Monika Henzinger, Alexander Svozil (LICS, 2021) ↗
Upper and Lower Bounds for Fully Retroactive Graph Problems. Monika Henzinger, Xiaowei Wu (WADS, 2021) ↗
A Survey of Bidding Games on Graphs (Invited Paper). Guy Avni, Thomas A. Henzinger (CONCUR, 2020) ↗
Approximating Values of Generalized-Reachability Stochastic Games. Pranav Ashok, Krishnendu Chatterjee, Jan Kretínský, Maximilian Weininger, Tobias Winkler (LICS, 2020) ↗
Constant-Time Dynamic (Δ+1)-Coloring. Monika Henzinger, Pan Peng (STACS, 2020) ↗
Deterministic Dynamic Matching in O(1) Update Time. Sayan Bhattacharya, Deeparnab Chakrabarty, Monika Henzinger (Algorithmica, 2020) ↗
Dynamic Approximate Maximum Independent Set of Intervals, Hypercubes and Hyperrectangles. Monika Henzinger, Stefan Neumann, Andreas Wiese (SoCG, 2020) ↗
Dynamic Clustering to Minimize the Sum of Radii. Monika Henzinger, Dariusz Leniowski, Claire Mathieu (Algorithmica, 2020) ↗
Dynamic Matching Algorithms in Practice. Monika Henzinger, Shahbaz Khan, Richard Paul, Christian Schulz (ESA, 2020) ↗
Fast Dynamic Cuts, Distances and Effective Resistances via Vertex Sparsifiers. Li Chen, Gramoz Goranci, Monika Henzinger, Richard Peng, Thatchaphol Saranurak (FOCS, 2020) ↗
Faster Algorithms for Quantitative Analysis of MCs and MDPs with Small Treewidth. Ali Asadi, Krishnendu Chatterjee, Amir Kafshdar Goharshady, Kiarash Mohammadi, Andreas Pavlogiannis (ATVA, 2020) ↗
Faster Fully Dynamic Transitive Closure in Practice. Kathrin Hanauer, Monika Henzinger, Christian Schulz (SEA, 2020) ↗
Finding All Global Minimum Cuts in Practice. Monika Henzinger, Alexander Noe, Christian Schulz, Darren Strash (ESA, 2020) ↗
Fully Dynamic Single-Source Reachability in Practice - An Experimental Study. Kathrin Hanauer, Monika Henzinger, Christian Schulz (ALENEX, 2020) ↗
Fully-Dynamic Coresets. Monika Henzinger, Sagar Kale (ESA, 2020) ↗
Improved Guarantees for Vertex Sparsification in Planar Graphs. Gramoz Goranci, Monika Henzinger, Pan Peng (SIAM J. Discret. Math., 2020) ↗
Induction with Generalization in Superposition Reasoning. Márton Hajdú, Petra Hozzová, Laura Kovács, Johannes Schoisswohl, Andrei Voronkov (CICM, 2020) ↗
Limits on amplifiers of natural selection under death-Birth updating. Josef Tkadlec, Andreas Pavlogiannis, Krishnendu Chatterjee, Martin A. Nowak (PLoS Comput. Biol., 2020) ↗
Local Flow Partitioning for Faster Edge Connectivity. Monika Henzinger, Satish Rao, Di Wang (SIAM J. Comput., 2020) ↗
Monitoring Event Frequencies. Thomas Ferrère, Thomas A. Henzinger, Bernhard Kragl (CSL, 2020) ↗
Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States. Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop (CONCUR, 2020) ↗
Optimal and Perfectly Parallel Algorithms for On-demand Data-Flow Analysis. Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, Andreas Pavlogiannis (ESOP, 2020) ↗
Outside the Box - Abstraction-Based Monitoring of Neural Networks. Thomas A. Henzinger, Anna Lukina, Christian Schilling (ECAI, 2020) ↗
Polynomial invariant generation for non-deterministic recursive programs. Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady (PLDI, 2020) ↗
Precedence-Aware Automated Competitive Analysis of Real-Time Scheduling. Andreas Pavlogiannis, Nico Schaumberger, Ulrich Schmid, Krishnendu Chatterjee (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2020) ↗
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., 2020) ↗
Shared-Memory Branch-and-Reduce for Multiterminal Cuts. Monika Henzinger, Alexander Noe, Christian Schulz (ALENEX, 2020) ↗
Simplified Game of Life - Algorithms and Complexity. Krishnendu Chatterjee, Rasmus Ibsen-Jensen, Ismaël Jecker, Jakub Svoboda (MFCS, 2020) ↗
Stochastic Games with Lexicographic Reachability-Safety Objectives. Krishnendu Chatterjee, Joost-Pieter Katoen, Maximilian Weininger, Tobias Winkler (CAV, 2020) ↗
Vienna Graph Clustering. Sonja Biedermann, Monika Henzinger, Christian Schulz, Bernhard Schuster (Protein-Protein Interaction Networks, 2020) ↗
A Deamortization Approach for Dynamic Spanner and Dynamic Maximal Matching. Aaron Bernstein, Sebastian Forster, Monika Henzinger (SODA, 2019) ↗
A New Deterministic Algorithm for Dynamic Set Cover. Sayan Bhattacharya, Monika Henzinger, Danupon Nanongkai (FOCS, 2019) ↗
Algorithms and Hardness for Diameter in Dynamic Graphs. Bertie Ancona, Monika Henzinger, Liam Roditty, Virginia Vassilevska Williams, Nicole Wein (ICALP, 2019) ↗
Bidding Mechanisms in Graph Games. Guy Avni, Thomas A. Henzinger, Dorde Zikelic (MFCS, 2019) ↗
Combinations of Qualitative Winning for Stochastic Parity Games. Krishnendu Chatterjee, Nir Piterman (CONCUR, 2019) ↗
Cost analysis of nondeterministic probabilistic programs. Peixin Wang, Hongfei Fu, Amir Kafshdar Goharshady, Krishnendu Chatterjee, Xudong Qin, Wenjun Shi (PLDI, 2019) ↗
Deciding Fast Termination for Probabilistic VASS with Nondeterminism. Tomás Brázdil, Krishnendu Chatterjee, Antonín Kucera, Petr Novotný, Dominik Velan (ATVA, 2019) ↗
Determinacy in Discrete-Bidding Infinite-Duration Games. Milad Aghajohari, Guy Avni, Thomas A. Henzinger (CONCUR, 2019) ↗
Distributed edge connectivity in sublinear time. Mohit Daga, Monika Henzinger, Danupon Nanongkai, Thatchaphol Saranurak (STOC, 2019) ↗
Efficient parameterized algorithms for data packing. Krishnendu Chatterjee, Amir Kafshdar Goharshady, Nastaran Okati, Andreas Pavlogiannis (Proc. ACM Program. Lang., 2019) ↗
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., 2019) ↗
Graph Planning with Expected Finite Horizon. Krishnendu Chatterjee, Laurent Doyen (LICS, 2019) ↗
Long-Run Average Behavior of Vector Addition Systems with States. Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop (CONCUR, 2019) ↗
Modular verification for almost-sure termination of probabilistic programs. Mingzhang Huang, Hongfei Fu, Krishnendu Chatterjee, Amir Kafshdar Goharshady (Proc. ACM Program. Lang., 2019) ↗
Near-Linear Time Algorithms for Streett Objectives in Graphs and MDPs. Krishnendu Chatterjee, Wolfgang Dvorák, Monika Henzinger, Alexander Svozil (CONCUR, 2019) ↗
New amortized cell-probe lower bounds for dynamic problems. Sayan Bhattacharya, Monika Henzinger, Stefan Neumann (Theor. Comput. Sci., 2019) ↗
Non-polynomial Worst-Case Analysis of Recursive Programs. Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady (ACM Trans. Program. Lang. Syst., 2019) ↗
Portfolio SAT and SMT Solving of Cardinality Constraints in Sensor Network Optimization. Gergely Kovásznai, Krisztián Gajdár, Laura Kovács (SYNASC, 2019) ↗
Quantitative Automata under Probabilistic Semantics. Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop (Log. Methods Comput. Sci., 2019) ↗
Shared-Memory Exact Minimum Cuts. Monika Henzinger, Alexander Noe, Christian Schulz (IPDPS, 2019) ↗
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, 2019) ↗
Superposition Reasoning about Quantified Bitvector Formulas. David Damestani, Laura Kovács, Martin Suda (SYNASC, 2019) ↗
Termination of Nondeterministic Probabilistic Programs. Hongfei Fu, Krishnendu Chatterjee (VMCAI, 2019) ↗
The Evolutionary Price of Anarchy - Locally Bounded Agents in a Dynamic Virus Game. Laura Schmid, Krishnendu Chatterjee, Stefan Schmid (OPODIS, 2019) ↗
The treewidth of smart contracts. Krishnendu Chatterjee, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady (SAC, 2019) ↗
Value-centric dynamic partial order reduction. Krishnendu Chatterjee, Andreas Pavlogiannis, Viktor Toman (Proc. ACM Program. Lang., 2019) ↗
