M. Frans Kaashoek
where else to find them
no profile links on file
what they talk about
where they keep going back
no series more than once — all 4 in the filters
on a stage with
all 9 in the filters
who talks about the same things
nobody close enough yet
| title | conference | date |
|---|---|---|
| Shipwright: A Modular Framework for Verifying Liveness of Byzantine Fault Tolerant(…) | Dafny 2025 | 2025-01-19 |
Shipwright is a Dafny framework that proves liveness of BFT systems by modular compositional refinement and novel completion measures. The project is ~12,000… | ||
| Verifying vMVCC, a high-performance transaction library using multi-version concurrency.. | OSDI 2023 | 2023-07-10 |
vMVCC claims to be the first MVCC transaction library with a machine-checked proof and ships as about 800 lines of Go (open source). It implements in-memory… | ||
| Leakage models are a leaky abstraction (...) | PLARCH 2023 | 2023-06-17 |
They verify timing by symbolically executing gate‑level RTL instead of assuming leakage models, translating circuits to Rosette and running a symbolic RTL… | ||
| GoJournal: a verified, concurrent, crash-safe journaling system | 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI '21) | 2021-07-14 |
GoJournal implements a verified, concurrent, crash-safe journaling API in Go and proves it in Coq with Perennial 2.0, using the Goose translator to model Go… | ||
| nothing matches | ||