Klaus von Gleissenthall

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

I am on the academic job market. 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.

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.

Publications

POPL'19	Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs. With Rami Gökhan Kici, Alexander Bakst, Deian Stefan and Ranjit Jhala. [PDF]
OOPSLA'17	Verifying Distributed Programs via Canonical Sequentialization. With Alexander Bakst, Rami Gökhan Kici and Ranjit Jhala.[PDF] [Slides] [Code] [Benchmarks] [ThequeFS] [Talk]
PLDI'16	Cardinalities and Universal Quantifiers for Verifying Parameterized Systems. With Nikolaj Bjørner and Andrey Rybalchenko.[PDF] [Slides] [Talk]
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.