Draft | Towards Constant-Time Foundations for the New Spectre Era. Sunjay Cauligi, Craig Disselkoen, Klaus v. Gleissenthall, Deian Stefan, Tamara Rezk, Gilles Barthe.[PDF][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. |