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

New: I'm recruiting a PhD student at the intersection of formal methods, PL and networking, together with Balakrishnan Chandrasekaran. Please get in touch if you are interested. The ininital review deadline is June 6. More info here.

I'm serving on the PC of ASPLOS'23.

I will give a talk at Commute which is co-located with PLDI'22.

Our paper on refinement types for hardware has been accepted at LATTE'22. You can watch the talk here.

Xenon, our paper on making timing verification of hardware more user-friendly was accepted to CCS'21.

I will be serving on the PCs of PLDI'22, CAV'22, CCSW'21, and PLAS'21.

🏆 Our paper on semantics for speculative execution was a finalist (honorable mention) in the intel hardware security award.

Check out our new blog post on Blade in Sigplan PL Perspective.

🏆 Blade wins distinguished paper award at POPL.

New draft: Solver-Aided Constant-Time Circuit Verification.

I will be serving on the PC of RAID'21.

I will be serving on the PC of CCS'21.

I will be serving on the PC of NETYS'21.

Blade accepted to POPL'21.

I'm co-chairing the VMCAI'21 artifact evaluation.

Our paper on speculative execution semantics has been accepted to PLDI'20.

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.

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:

2023	ASPLOS
2022	PLDI, CAV
2021	CCS, NETYS, RAID, CCSW, PLAS
2020	PriSC
2019	PLAS

Co-Chairing & Organization:

2021	VMCAI Artifact Evaluation
2019	Verification of Distributed Systems Workshop (VDS)

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.