Klaus von Gleissenthall

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

My research focuses on (automated) methods for proving the correctness of programs. I am paricularly interested in applying these methods to facilitate reasoning about concurrency and for the verification of security related program 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.

For my MSc. thesis, I worked on characterizing consistency conditions of distributed systems (like eventual consistency) in terms of epistemic logic (i.e., the logic of knowledge). This work examines the question of what correctness of a computation means from the point of view of the threads/nodes taking part in it.


OOPSLA'17 Verifying Distributed Programs via Canonical Sequentialization. With Alexander Bakst, Rami Gökhan kici and Ranjit Jhala.[PDF]
PLDI'16 Cardinalities and Universal Quantifiers for Verifying Parameterized Systems. With Nikolaj Bjørner and Andrey Rybalchenko.[PDF] [Slides]
CAV'15 Symbolic Polytopes for Quantitative Interpolation and Verification. With Boris Köpf and Andrey Rybalchenko.
[PDF] [Slides] [Extended Version]
CONCUR'13 An Epistemic Perspective on Consistency of Concurrent Computations. With Andrey Rybalchenko. [PDF] [Slides]
KI'11 Bayesian Logic Networks and the Search for Samples with Backward Simulation and Abstract Constraint Learning. With Dominik Jain and Michael Beetz.

See also my DBLP entry.