From 2d197c30b26e1c7263209afe5693bd6930f37c08 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Tue, 5 May 2026 06:46:48 -0700 Subject: [PATCH] Added video links for all presentations in the 2026 ETAPS schedule. Signed-off-by: Markus Alexander Kuppe --- content/2026-etaps/_index.md | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/content/2026-etaps/_index.md b/content/2026-etaps/_index.md index f794847..686712c 100644 --- a/content/2026-etaps/_index.md +++ b/content/2026-etaps/_index.md @@ -22,20 +22,20 @@ Torino, Italy
| time | title | speaker | affiliation | slides | recording | |------|--------|---------|--------|------------|-----| -| 09:00 | A Compositional Strategy for Verifying Fault-Tolerant Dynamic Task Graph Scheduling in Modern Cloud Environments | [Quentin Delamea](https://fr.linkedin.com/in/quentin-delamea-380a67198) | Aneo & Univ. Saclay | [ppt](delamea-2026.ppsx) [pdf](delamea-2026.pdf) -| 09:30 | A generic hardware in-order pipeline architecture model to capture key temporal properties | [Mamoun Filali](https://www.researchgate.net/profile/Mamoun-Filali) | CNRS & IRIT | [slides](filali-2026.pdf) +| 09:00 | A Compositional Strategy for Verifying Fault-Tolerant Dynamic Task Graph Scheduling in Modern Cloud Environments | [Quentin Delamea](https://fr.linkedin.com/in/quentin-delamea-380a67198) | Aneo & Univ. Saclay | [ppt](delamea-2026.ppsx) [pdf](delamea-2026.pdf) | [video](https://www.youtube.com/watch?v=84js0u7t2_g) +| 09:30 | A generic hardware in-order pipeline architecture model to capture key temporal properties | [Mamoun Filali](https://www.researchgate.net/profile/Mamoun-Filali) | CNRS & IRIT | [slides](filali-2026.pdf) | [video](https://www.youtube.com/watch?v=YhHvzS_67wM) | _10:00_ | *Coffee Break* -| 10:30 | Extensible Proof Decomposition Rules for TLAPS | [Karolis Petrauskas](https://www.researchgate.net/profile/Karolis-Petrauskas) | Vilnius University | [slides](petrauskas-2026.pdf) -| 11:00 | Systematic API Testing through Model Checking and Executable Contracts | [Ana Catarina Ribeiro](https://pt.linkedin.com/in/acm-ribeiro) | NOVA University, Lisbon | [slides](ribeiro-2026.pdf) -| 11:30 | Model-based Testing of Practical Distributed Systems in Actor Model | [Ilya Kokorin](https://www.linkedin.com/in/ilyambda/) | ITMO University | [slides](kokorin-2026.pdf) -| 12:00 | Interactive symbolic testing with TLA+, Apalache, and LLMs | [Igor Konnov](https://konnov.phd) | | [slides](konnov-2026.pdf) +| 10:30 | Extensible Proof Decomposition Rules for TLAPS | [Karolis Petrauskas](https://www.researchgate.net/profile/Karolis-Petrauskas) | Vilnius University | [slides](petrauskas-2026.pdf) | [video](https://www.youtube.com/watch?v=tDcBCLqFmVM) +| 11:00 | Systematic API Testing through Model Checking and Executable Contracts | [Ana Catarina Ribeiro](https://pt.linkedin.com/in/acm-ribeiro) | NOVA University, Lisbon | [slides](ribeiro-2026.pdf) | [video](https://www.youtube.com/watch?v=mpQHBtvvPvQ) +| 11:30 | Model-based Testing of Practical Distributed Systems in Actor Model | [Ilya Kokorin](https://www.linkedin.com/in/ilyambda/) | ITMO University | [slides](kokorin-2026.pdf) | [video](https://www.youtube.com/watch?v=iPEE0s64pY4) +| 12:00 | Interactive symbolic testing with TLA+, Apalache, and LLMs | [Igor Konnov](https://konnov.phd) | | [slides](konnov-2026.pdf) | [video](https://www.youtube.com/watch?v=CQPhAfi-6Uk) | _12:30_ | *Lunch Break* -| 14:00 | Thinking in TLA+ – Modeling Judgment for System Design | [Murat Demirbas](https://muratbuffalo.blogspot.com) | MongoDB | [slides](demirbas-2026.pdf) -| 14:50 | P2P2P (PlusCal to PlantUML to PDF) | [Juan José Serrano Mora](https://www.linkedin.com/in/juan-josé-serrano-mora/) | Northern Arizona University | [slides](mora-2026.pdf) -| 15:20 | Towards Language Model Guided TLA+ Proof Automation | [Yuhao Zhou](https://www.khoury.northeastern.edu/home/yuhaoz/index.html) | Northeastern University | [slides](zhou-2026.pdf) +| 14:00 | Thinking in TLA+ – Modeling Judgment for System Design | [Murat Demirbas](https://muratbuffalo.blogspot.com) | MongoDB | [slides](demirbas-2026.pdf) | [video](https://www.youtube.com/watch?v=1AjXfyw4MM4) +| 14:50 | P2P2P (PlusCal to PlantUML to PDF) | [Juan José Serrano Mora](https://www.linkedin.com/in/juan-josé-serrano-mora/) | Northern Arizona University | [slides](mora-2026.pdf) | [video](https://www.youtube.com/watch?v=gILKvGZiWgM) +| 15:20 | Towards Language Model Guided TLA+ Proof Automation | [Yuhao Zhou](https://www.khoury.northeastern.edu/home/yuhaoz/index.html) | Northeastern University | [slides](zhou-2026.pdf) | [video](https://www.youtube.com/watch?v=-8wV7-qd6js) | _16:00_ | *Coffee Break* -| 16:30 | Verifying differential privacy in TLA+ via self-products | [Ugur Yavuz](https://uguryav.uz) | Boston University | [slides](yavuz-2026.pdf) -| 17:00 | Veil: Multi-Modal Verification of Transition Systems | [George Pîrlea](https://pirlea.net) | National University of Singapore | [slides](pirlea-2026.pdf) +| 16:30 | Verifying differential privacy in TLA+ via self-products | [Ugur Yavuz](https://uguryav.uz) | Boston University | [slides](yavuz-2026.pdf) | [video](https://www.youtube.com/watch?v=-lp1p-gcx9I) +| 17:00 | Veil: Multi-Modal Verification of Transition Systems | [George Pîrlea](https://pirlea.net) | National University of Singapore | [slides](pirlea-2026.pdf) | [video](https://www.youtube.com/watch?v=24mMfUSCyto) | 17:30 | Roundtable & closing | 19:30 | Workshop dinner