Skip to content

Commit ad487c1

Browse files
committed
Upload first set of slides TLA+ Community Event 2025
1 parent 9edadc4 commit ad487c1

File tree

5 files changed

+8
-8
lines changed

5 files changed

+8
-8
lines changed

content/2025-etaps/_index.md

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -45,17 +45,17 @@ Participants will be required to register to ETAPS 2025.
4545
| time | title | speaker | affiliation | slides | recording |
4646
|------|--------|---------|--------|------------|-----|
4747
| 09:00 | Welcome & Opening Announcements | | | | |
48-
| 09:15 | *ModelFuzz: Model guided fuzzing of distributed systems* | [Srinidhi Nagendra](https://www.srinidhin.com) | Max Planck Institute for Software Systems | [pdf](nagendra.pdf) | [video](https://youtu.be/dMfZHAXDU78) |
48+
| 09:15 | *ModelFuzz: Model guided fuzzing of distributed systems* | [Srinidhi Nagendra](https://www.srinidhin.com) | Max Planck Institute for Software Systems | [abstract](nagendra.pdf), [slides](nagendra-slides.pdf) | [video](https://youtu.be/dMfZHAXDU78) |
4949
| _10:00_ | *Coffee Break* | | | | |
50-
| 10:30 | *Automating Trace Validation with PGo* | [Finn Hackett](https://fhackett.com) & [Ivan Beschastnikh](https://www.cs.ubc.ca/~bestchai/) | University of British Columbia | [pdf](hackett.pdf) | |
51-
| 11:15 | *Translating C to PlusCal for Model Checking of Safety Properties on Source Code* | [Guillaume DI FATTA](https://www.linkedin.com/in/guillaume-di-fatta-0441a3253/), [Emmanuel Ohayon](https://scholar.google.fr/citations?user=nYVf510AAAAJ&hl=fr), and [Amira Methni](https://dblp.org/pid/167/5040.html)| Asterios Technologies | [pdf](di-fatta.pdf) | [video](https://youtu.be/0A5qMWvFgdI) |
52-
| 12:00 | *TLA+ for All: Model Checking in a Python Notebook* | [Konstantin Läufer](https://laufer.cs.luc.edu) & [George K. Thiruvathukal](https://gkt.sh) | Loyola University Chicago | [pdf](laufer.pdf) | |
50+
| 10:30 | *Automating Trace Validation with PGo* | [Finn Hackett](https://fhackett.com) & [Ivan Beschastnikh](https://www.cs.ubc.ca/~bestchai/) | University of British Columbia | [abstract](hackett.pdf), [slides](hackett-slides.pdf) | |
51+
| 11:15 | *Translating C to PlusCal for Model Checking of Safety Properties on Source Code* | [Guillaume DI FATTA](https://www.linkedin.com/in/guillaume-di-fatta-0441a3253/), [Emmanuel Ohayon](https://scholar.google.fr/citations?user=nYVf510AAAAJ&hl=fr), and [Amira Methni](https://dblp.org/pid/167/5040.html)| Asterios Technologies | [abstract](di-fatta.pdf), [slides](di-fatta-slides.pdf) | [video](https://youtu.be/0A5qMWvFgdI) |
52+
| 12:00 | *TLA+ for All: Model Checking in a Python Notebook* | [Konstantin Läufer](https://laufer.cs.luc.edu) & [George K. Thiruvathukal](https://gkt.sh) | Loyola University Chicago | [abstract](laufer.pdf), [slides]() | |
5353
| _12:30_ | *Lunch* | | | | |
54-
| 14:00 | *Formal models for monotonic pipeline architectures* | [J.-P. Bodeveix](https://dblp.org/pid/97/1837.html), [A. Bonenfant](https://scholar.google.fr/citations?user=8k2MVLYAAAAJ&hl=fr), [T. Carle](https://scholar.google.fr/citations?user=3iKALIoAAAAJ&hl=sr), [M. Filali](https://dblp.org/pid/60/599.html), [C. Rochange](https://www.irit.fr/~Christine.Rochange/) | | [pdf](filali.pdf) | |
55-
| 14:45 | *TLA+ Modeling of MongoDB Transactions* | [Murat Demirbas](https://www.linkedin.com/in/murat-demirbas-distributolog-a2233b176/) & [Will Schultz](https://www.linkedin.com/in/william-schultz-a22714a2/) | MongoDB | [pdf](demirbas.pdf) | |
56-
| 15:30 | *Are We Serious About Using TLA+ For Statistical Properties?* | [A. Jesse Jiryu Davis](https://emptysqua.re) | MongoDB | [txt](davis.txt) | |
54+
| 14:00 | *Formal models for monotonic pipeline architectures* | [J.-P. Bodeveix](https://dblp.org/pid/97/1837.html), [A. Bonenfant](https://scholar.google.fr/citations?user=8k2MVLYAAAAJ&hl=fr), [T. Carle](https://scholar.google.fr/citations?user=3iKALIoAAAAJ&hl=sr), [M. Filali](https://dblp.org/pid/60/599.html), [C. Rochange](https://www.irit.fr/~Christine.Rochange/) | | [abstract](filali.pdf), [slides]() | |
55+
| 14:45 | *TLA+ Modeling of MongoDB Transactions* | [Murat Demirbas](https://www.linkedin.com/in/murat-demirbas-distributolog-a2233b176/) & [Will Schultz](https://www.linkedin.com/in/william-schultz-a22714a2/) | MongoDB | [abstract](demirbas.pdf), [slides](demirbas-slides.pdf) | |
56+
| 15:30 | *Are We Serious About Using TLA+ For Statistical Properties?* | [A. Jesse Jiryu Davis](https://emptysqua.re) | MongoDB | [txt](davis.txt), [slides]() | |
5757
| _16:00_ | *Coffee Break* | | | | |
58-
| 16:30 | *It's never been easier to write TLA⁺ tooling!* | [Andrew Helwer](https://www.linkedin.com/in/ahelwer/) | | [txt](helwer.txt) | |
58+
| 16:30 | *It's never been easier to write TLA⁺ tooling!* | [Andrew Helwer](https://www.linkedin.com/in/ahelwer/) | | [txt](helwer.txt), [slides]() | |
5959
| 17:00 | Discussion Panel, Announcements, and Closing Remarks | | | | |
6060
| 17:30 | End of the conference | | | | |
6161

2.3 MB
Binary file not shown.
602 KB
Binary file not shown.
1.06 MB
Binary file not shown.
5.33 MB
Binary file not shown.

0 commit comments

Comments
 (0)