Klaus von Gleissenthall
I am a post-doc in the Programming
group at UCSD
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
. This is my
Before coming to UCSD I was a PhD student at
where I was advised by Andrey
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
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.
||Verifying Distributed Programs via Canonical
Sequentialization. With Alexander Bakst, Rami Gökhan kici and
||Cardinalities and Universal Quantifiers for Verifying
Parameterized Systems. With Nikolaj Bjørner and Andrey
|| Symbolic Polytopes for Quantitative Interpolation and
Verification. With Boris Köpf and Andrey Rybalchenko.
[Slides] [Extended Version]
|| An Epistemic Perspective on Consistency of Concurrent
Computations. With Andrey Rybalchenko. [PDF] [Slides]
||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