TLA+ Community Event 2020
| title | author | length |
|---|---|---|
| Conjunction Capers: A TLA+ Truffle | Ron Pressler | 27m |
Shows two concrete uses of composing canonical TLA+ state‑machines and how to run them in TLC by rewriting Next into a single boxed action (putting UNCHANGED… | ||
| An Extension of PlusCal for Modeling Distributed Algorithms | Heba Alkayed et al. | 10m |
An extension called distributed PlusCal adds nested sub-processes and first-class channel types so a single process models a node with a main thread plus a… | ||
| Higher-order Automation In TLAPS | Antoine Defourné, Petar Vukmirovic | 14m |
Implements a direct THF export from TLA+ and adds Zipperposition as a higher-order backend, so TLAPS no longer needs heavy eliminations for… | ||
| A Formal Model of Cache Speculation Side-Channels | Catalin Marinas | 20m |
A TLA+ specification models speculative execution as two-CPU speculative model sharing memory and a single cached/not-cached bit per address, with… | ||
| eXtreme Modelling in Practice | Jesse Davis, Max Hirschhorn, Judah Schvimer | 22m |
Two case studies compare two conformance techniques applied with TLA+ and TLC. model-based trace checking against the MongoDB Server fails after ten weeks… | ||
| Checking safety in Exactly-once | Tomek Masternak, Szymon Pobiega | 25m |
Exactly-once is a library that implements atomic commit between business state in Azure Cosmos DB and output messages sent from Azure Functions, relying on… | ||
| Type Inference For TLA+ in Apalache | Jure Kukovec, Igor Konnov | 40m |
Apalache ships two standalone tools: a type checker that performs local analysis and asks for a few annotations (used in the CarTalkPuzzle demo with four… | ||
| Exploring and improving the design of Abaco | Smruti Padhy, Joe Stubbs | 28m |
They build a TLA+ spec and run the TLC model checker to expose a race that lets new executions start with stale container images on Abaco, a production FaaS… | ||
| TLA + specification of PCR parallel programming pattern | Jose Solsona, Sergio Yovine | 32m |
Formalizes the Produce-Consume-Reduce parallel skeleton as a family of TLA+ modules and models concrete examples (fibPrimes1 and fibPrimes2) with nested PCRs… | ||
| Model-based testing with TLA+ and Apalache | Andrey Kupriyanov, Igor Konnov | 30m |
Model-based testing uses TLA+ assertions and the Apalache model checker to auto-generate JSON counterexamples, transform them (via JSONata and… | ||
| Bridging the Verifiability Gap: Why We Need More From Our Specs and How We Get It | Jordan Haltermann | 19m |
ONOS goes from research to nationwide Comcast deployment while teams spend hours scanning gigabytes of logs to find elusive distributed bugs. The workflow… | ||
| TLA+ validation of Chord | Jean-Paul Bodeveix, Julien Brunel, David Chemouil, Mamoun Filali | 20m |
Mechanized TLA+ model and Isabelle proofs validate Chord maintenance: the model, fully mechanized in Isabelle-TLA with a Principals theory in Isabelle‑HOL… | ||
| Kayfabe: Model-based program testing with TLC | Star Dorminey | 23m |
Kayfabe is a C# harness that runs TLC, extracts the full TLC state graph, computes a minimal spanning set of behaviors by reducing routing to TSP (NP‑hard) and… | ||
| TLA+ at Microsoft to build planetary-scale systems | Dharma Shukla | 34m |
Microsoft uses TLA+ to specify and validate concrete designs for Cosmos DB and a global AI scheduler, producing five consistency levels formally specified and… | ||
| nothing matches | ||