Klaus von Gleissenthall

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

Application Material: Here are my Research Statement, Teaching Statement and CV. (updated Jan 10).

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.



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.


Draft Automatically Eliminating Speculative Leaks with Blade. Marco Vassena, Klaus v. Gleissenthall, Rami Gökhan Kici, Deian Stefan and Ranjit Jhala. [PDF]
Draft Towards Constant-Time Foundations for the New Spectre Era. Sunjay Cauligi, Craig Disselkoen, Klaus v. Gleissenthall, Deian Stefan, Tamara Rezk, Gilles Barthe.[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.