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.

News

Iodine accepted at Usenix Security'19.
I'm serving on the Artifact Evaluation Committee of CAV'20.
Visited MPI-SWS and INRIA Méditerranée.
Attended the Open-source enclaves workshop in Berkeley.
I'm co-orgranizing the Workshop on Verification of Distributed Systems (VDS)'19.
I'm serving on the PC of PLAS'19.
I'm serving on the PC of PriSC'20.

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.

Publications

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.