I work on methods that help practitioners write correct, secure and reliable
systems, where I focus on keeping user effort low. My research interests
span programming languages, security and systems.
.
I'm looking for students at all levels. I have open positions for PhDs, and post-docs. If you're interested in the intersection of Security, Programming Languages and Formal Verification, please email me.
scholarship. During my PhD I worked at
as an intern and
spent some more time there as a visitor. I received both a BSc. and MSc.
in computer science from TUM with a minor in logic and philosophy of science at
. During my master's, I spent five months at
OOPSLA'24 |
Refinement Type Refutations. Robin Webbers, Klaus v. Gleissenthall, Ranjit Jhala. [PDF] |
IEEE TDSC'24 |
InvisiGuard: Data Integrity for Microcontroller-Based
Devices via Hardware-Triggered Write Monitoring.
Dongliang Fang, Anni Peng, Le Guan, Erik van der Kouwe, Klaus v. Gleissenthall, Wenwen Wang, Yuqing Zhang, Limin Sun. [PDF] |
CCS'23 |
Specification and Verification of Side-channel Security for
Open-source Processors via Leakage Contracts. Zilong Wang, Gideon Mohr, Klaus v. Gleissenthall, Jan Reineke, Marco Guarnieri. Distinguished Paper Award. 🏆 [PDF] |
PLDI'23 |
Don't Look UB: Exposing Sanitizer-Eliding Compiler Optimizations. Raphael Isemann, Cristiano Giuffrida, Herbert Bos, Erik van der Kouwe, Klaus v. Gleissenthall.[PDF] |
ACSAC'23 |
Triereme: Speeding up hybrid fuzzing through efficient query scheduling. Elia Geretto, Julius Hohnerlein, Cristiano Giuffrida, Herbert Bos, Erik Van Der Kouwe, Klaus v. Gleissenthall.[PDF] |
OOPSLA'23 |
Randomized Testing of Byzantine Fault Tolerant Algorithms. L. Winter, F. Buse, D. de Graaf, Klaus v. Gleissenthall, B. Kulahcioglu Ozkan. Distinguished Paper Award. 🏆 [PDF] |
LATTE'22 |
Refinement Types for Hardware. Robin Webbers, Klaus v. Gleissenthall. |
CCS'21 |
Solver-Aided Constant-Time Hardware Verification. Klaus v. Gleissenthall, Rami Gökhan Kici, Deian Stefan and Ranjit Jhala. [PDF] |
POPL'21 |
Automatically Eliminating Speculative Leaks with Blade. Marco Vassena, Craig Disselkoen, Klaus v. Gleissenthall,
Sunjay Cauligi, Rami Gökhan Kici, Dean Tullsen, Ranjit Jhala, Deian Stefan.
Distinguished Paper Award. 🏆
[PDF][Code] [LLVM Blade] |
PLDI'20 |
Towards Constant-Time Foundations for the New Spectre Era. Sunjay Cauligi, Craig Disselkoen, Klaus v. Gleissenthall,
Dean Tullsen, Deian Stefan, Tamara Rezk, Gilles Barthe. Honorable mention, Intel hardware security award. 🏆 [PDF][Talk][Code] |
USENIX Security'19 |
IODINE: Verifying Constant-Time Execution of Hardware. Klaus v. Gleissenthall, Rami Gökhan Kici, Deian Stefan and
Ranjit Jhala. [PDF][Slides][Code][Talk]
|
POPL'19 |
Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs. Klaus v. Gleissenthall, Rami Gökhan Kici, Alexander Bakst, Deian Stefan and
Ranjit Jhala. [PDF][Slides][Code]
|
OOPSLA'17 |
Verifying Distributed Programs via Canonical
Sequentialization. With Alexander Bakst, Klaus v. Gleissenthall, Rami Gökhan Kici and
Ranjit Jhala.[PDF]
[Slides]
[Code]
[Benchmarks]
[ThequeFS]
[Talk]
|
PLDI'16 |
Cardinalities and Universal Quantifiers for Verifying
Parameterized Systems. Klaus v. Gleissenthall, Nikolaj Bjørner and Andrey
Rybalchenko.[PDF]
[Slides]
[Talk]
|
CAV'15 |
Symbolic Polytopes for Quantitative Interpolation and
Verification. Klaus v. Gleissenthall, Boris Köpf and Andrey Rybalchenko.
[PDF]
[Slides] [Extended Version]
|
CONCUR'13 |
An Epistemic Perspective on Consistency of Concurrent
Computations. Klaus v. Gleissenthall and Andrey Rybalchenko. [PDF] [Slides] |
KI'11 |
Bayesian Logic Networks and the Search for Samples with Backward
Simulation and Abstract Constraint Learning. Dominik Jain, Klaus v. Gleissenthall and Michael Beetz. |