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.
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.
News
Bio
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.
Service
Program Committees:
Co-Chairing & Organization:
Publications
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.