Klaus von Gleissenthall
I am a postdoc 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.
Bio
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.
Publications
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.