Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 11 additions & 11 deletions content/2026-etaps/_index.md
Original file line number Diff line number Diff line change
Expand Up @@ -22,20 +22,20 @@ Torino, Italy<br>

| 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

Expand Down
Loading