Klaus von Gleissenthall

I am an Assistant Professor in Computer Science at the Vrije Universiteit Amsterdam, where I am affiliated with the theory group and VUSec.

I work on methods that help practitioners write correct, secure and reliable systems, where I focus on keeping user effort low. My research interests span programming languages, security and systems.

Here is my CV.

Send me an email here.

I'm also archiving my application material: Research Statement and Teaching Statement.

If you click on the photo, there'll be more pictures.

New: I'm looking for students at all levels, and we have open positions for PhDs, and post-docs. If you're interested in the intersection of Security, Programming Languages and Formal Verification, please email me.



Before coming to the VU, I was a post-doc in the Programming Systems group at UCSD where I worked with Ranjit Jhala and Deian Stefan. Before that, 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 spent some more time there as a visitor. 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 months at Université Paris Diderot.


Program Committees:

Co-Chairing & Organization:
2021VMCAI Artifact Evaluation
2019Verification of Distributed Systems Workshop (VDS)


CCS'21 Solver-Aided Constant-Time Hardware Verification. Klaus v. Gleissenthall, Rami Gökhan Kici, Deian Stefan and Ranjit Jhala. [PDF]
POPL'21 Automatically Eliminating Speculative Leaks with Blade. Marco Vassena, Craig Disselkoen, Klaus v. Gleissenthall, Sunjay Cauligi, Rami Gökhan Kici, Dean Tullsen, Ranjit Jhala, Deian Stefan. Distinguished Paper Award. 🏆 [PDF][Code]
PLDI'20 Towards Constant-Time Foundations for the New Spectre Era. Sunjay Cauligi, Craig Disselkoen, Klaus v. Gleissenthall, Dean Tullsen, Deian Stefan, Tamara Rezk, Gilles Barthe. Honorable mention, Intel hardware security award. 🏆 [PDF][Talk][Code]
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.

See also my DBLP entry.