Klaus von Gleissenthall

I am a post-doc in the Programming Systems group at UCSD where I work with Ranjit Jhala.

Here are my Research Statement and Teaching Statement.

My research focuses on (automated) methods that make it easier to implement correct and performant software systems. I am paricularly interested in applying these methods to facilitate reasoning about concurrent and distributed systems and for the verification of security related properties.

My email address is gleissen@ucsd.edu. This is my CV.



Before coming to UCSD, I was a PhD student at TUM where I was advised by Andrey Rybalchenko and funded through a Microsoft Research scholarship. During my PhD I worked at Microsoft Research Cambridge as an intern and contractor and spent some more time there as a visitor. Before that, I received both a BSc. and MSc. in computer science from TUM with a minor in logic and philosophy of science at LMU. During my master's, I spent five month at Université Paris Diderot.

For my PhD I worked on verification methods that track cardinalities of sets. Reasoning about cardinalities is needed in distributed systems where correctness arguments often rely on counting the number of processes that are in a given state. Another application is quantifying information flow where one needs to reason about the amount of secret information leaked to an attacker.


Draft Towards Constant-Time Foundations for the New Spectre Era. Sunjay Cauligi, Craig Disselkoen, Klaus v. Gleissenthall, Deian Stefan, Tamara Rezk, Gilles Barthe.[PDF][Arxiv]
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.

See also my DBLP entry.