Skip to content

Commit 71eff77

Browse files
committed
Next batch of talks and slides
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
1 parent 48aed06 commit 71eff77

File tree

4 files changed

+4
-4
lines changed

4 files changed

+4
-4
lines changed

content/2025-etaps/_index.md

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -49,13 +49,13 @@ Participants will be required to register to ETAPS 2025.
4949
| _10:00_ | *Coffee Break* | | | | |
5050
| 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) | [video](https://youtu.be/MLvLQ4p9je4) |
5151
| 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), [Q&A](https://youtu.be/NgYIS02EUnI) |
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]() |[video](https://youtu.be/726oDQQRxBQ) |
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](laufer-slides.pdf) |[video](https://youtu.be/726oDQQRxBQ) |
5353
| _12:30_ | *Lunch* | | | | |
5454
| 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]() | [video](https://youtu.be/6mTGeNVkKZo) |
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) | [video]() |
56-
| 15:30 | *Are We Serious About Using TLA+ For Statistical Properties?* | [A. Jesse Jiryu Davis](https://emptysqua.re) | MongoDB | [txt](davis.txt), [slides]() | [video]() |
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) | [video](https://youtu.be/fIWUo4gzvNE) |
56+
| 15:30 | *Are We Serious About Using TLA+ For Statistical Properties?* | [A. Jesse Jiryu Davis](https://emptysqua.re) | MongoDB | [txt](davis.txt), [slides](davis-slides.pdf) | [video](https://youtu.be/Wekywox2Ghk) |
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), [slides]() | [video]() |
58+
| 16:30 | *It's never been easier to write TLA⁺ tooling!* | [Andrew Helwer](https://www.linkedin.com/in/ahelwer/) | | [txt](helwer.txt), [slides](helwer-slides.odp) | [video](https://youtu.be/KrhZebeRn90) |
5959
| 17:00 | Discussion Panel, Announcements, and Closing Remarks | | | | |
6060
| 17:30 | End of the conference | | | | |
6161

static/2025-etaps/davis-slides.pdf

18.1 MB
Binary file not shown.
1.33 MB
Binary file not shown.
822 KB
Binary file not shown.

0 commit comments

Comments
 (0)