Markus A Kuppe
where else to find them
what they talk about
where they keep going back
no series more than once — all 5 in the filters
on a stage with
- A. Finn Hackettonce
- Amaury Chamayouonce
- Edward Ashtononce
all 5 in the filters
who talks about the same things
- Hillel Wayne9 talks
- Pawel Szulc28 talks
- Chelsea Troy9 talks
- Sharon Shoham13 talks
- Hiroshi Unno18 talks
- Thomas Reps20 talks
| title | conference | date |
|---|---|---|
| Smart Casual Verification of the Confidential Consortium Framework | NSDI '25 | 2025-04-28 |
Specifies CCF's distributed consensus and client-consistency model in TLA+, instruments the C++ code to emit tiny JSON state traces, and repurposes the TLC… | ||
| Weeks of Debugging Can Save You Hours of TLA+ | Craft Conference 2023 | 2023-05-18 |
A TLA+ model of a simple webshop reproduces a real-world bug: after about 1800 reads the backend sometimes sees no order because replication lag plus the wrong… | ||
| Turning an Incident Report into a Design Issue with TLA+ | SREcon23 Americas | 2023-03-21 |
A precise TLA+ specification of Cosmos DB behavior reproduces the 28-day outage as a counterexample and shows the root cause is missing session tokens between… | ||
| Workshop: TLA+ in action (Part 1) | Hydra 2021 | 2021-06-15 |
Workshop builds a TLA+ specification of Safra’s EWD998 termination detector, iterates from a token-free counter to the token+count version, and exercises the… | ||
| Workshop: TLA+ in action (Part 2) | Hydra 2021 | 2021-06-15 |
Workshop models Safra’s EWD998 termination detector in TLA+ using TLC model checking and Lamport’s tutorial style, exercises include reducing Naturals to a… | ||
| Workshop: TLA+ in action (Part 3) | Hydra 2021 | 2021-06-15 |
A runnable TLA+ model of Dijkstra/Safra EWD998 appears, modeling node color and per-node counters, a token record with position Q and color, and message… | ||
| Workshop: TLA+ in action (Part 4) | Hydra 2021 | 2021-06-15 |
Workshop models EWD998 termination detection in TLA+, writes a low‑level spec that replaces counters with inboxes and a recursive sum, and checks safety and… | ||
| Weeks of Debugging Can Save You Hours of TLA+ | SREcon20 Americas | 2020-12-07 |
A TLA+ spec of a bounded MPMC queue reproduces and explains a surprising deadlock that unit tests miss: TLC finds a violating trace (shortest 9 steps, another… | ||
| nothing matches | ||