Skip to content

Commit 47739e4

Browse files
deploy: 56976d8
1 parent c8436f8 commit 47739e4

6 files changed

Lines changed: 1 addition & 1 deletion

File tree

2026-etaps/demirbas-2026.pdf

214 KB
Binary file not shown.

2026-etaps/index.html

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
parent
33
active"><a href=/2026-etaps/>2026 - TLA+ Community Event</a></li><li data-nav-id=/2025-etaps/ title="2025 - TLA+ Community Event" class=dd-item><a href=/2025-etaps/>2025 - TLA+ Community Event</a></li><li data-nav-id=/2024-fm/ title="2024 - TLA+ Community Event" class=dd-item><a href=/2024-fm/>2024 - TLA+ Community Event</a></li><li data-nav-id=/2024/ title="2024 - TLA+ Conf" class=dd-item><a href=/2024/>2024 - TLA+ Conf</a></li><li data-nav-id=/2023/ title="2023 - TLA+ Community Event" class=dd-item><a href=/2023/>2023 - TLA+ Community Event</a><ul><li data-nav-id=/2023/dragoischwiderski/ title class=dd-item><a href=/2023/dragoischwiderski/></a></li><li data-nav-id=/2023/olivierconstant/ title class=dd-item><a href=/2023/olivierconstant/></a></li></ul></li><li data-nav-id=/2022/ title="2022 - TLA+ Conf" class=dd-item><a href=/2022/>2022 - TLA+ Conf</a><ul></ul></li><li data-nav-id=/202110/ title="2021 - TLA+ Tutorial" class=dd-item><a href=/202110/>2021 - TLA+ Tutorial</a></li><li data-nav-id=/2021/ title="2021 - TLA+ Conf" class=dd-item><a href=/2021/>2021 - TLA+ Conf</a><ul></ul></li><li data-nav-id=/2020/ title="2020 - TLA+ Community Event" class=dd-item><a href=/2020/>2020 - TLA+ Community Event</a></li><li data-nav-id=/2019/ title="2019 - TLA+ Conf" class=dd-item><a href=/2019/>2019 - TLA+ Conf</a><ul></ul></li><li data-nav-id=/2018/ title="2018 - TLA+ Community Event" class=dd-item><a href=/2018/>2018 - TLA+ Community Event</a><ul></ul></li><li data-nav-id=/2014/ title="2014 - TLA+ Community Event" class=dd-item><a href=/2014/>2014 - TLA+ Community Event</a><ul></ul></li><li data-nav-id=/2012/ title="2012 - TLA+ Community Event" class=dd-item><a href=/2012/>2012 - TLA+ Community Event</a></li></ul><section id=footer><h4>Contact</h4>"tla2024" \o "@" \o "tlapl.us"</section></div></nav><section id=body><div id=overlay></div><div class="padding highlightable sticky-parent"><div class=sticky-spacer><div><div id=breadcrumbs itemscope itemtype=http://data-vocabulary.org/Breadcrumb><span id=sidebar-toggle-span><a href=# id=sidebar-toggle data-sidebar-toggle><i class="fa fa-bars"></i></a></span>
44
<span id=toc-menu><i class="fa fa-list-alt"></i></span>
5-
<span class=links><a href=/>TLA+ Community Event & Conference</a> > 2026 - TLA+ Community Event</span></div><div class=progress><div class=wrapper><nav id=TableOfContents><ul><li><ul><li><a href=#co-located-with-etaps-2026httpsetapsorg2026-in-torino-italy-on-april-12-2026>Co-located with <a href=https://etaps.org/2026/>ETAPS 2026</a> in Torino, Italy, on April 12, 2026.</a></li><li><a href=#schedule>Schedule</a></li><li><a href=#call-for-presentations>Call for presentations</a></li><li><a href=#organizers>Organizers</a></li></ul></li></ul></nav></div></div></div></div><div id=body-inner><div align=right><h4><p>TLA<sup>+</sup> Community Event 2026<br>Sunday, April 12, 2026<br>Torino, Italy<br></p></h4></div><h1 id=tla-community-event-2026>TLA+ Community Event 2026</h1><h3 id=co-located-with-etaps-2026httpsetapsorg2026-in-torino-italy-on-april-12-2026>Co-located with <a href=https://etaps.org/2026/>ETAPS 2026</a> in Torino, Italy, on April 12, 2026.</h3><h3 id=schedule>Schedule</h3><table><thead><tr><th>time</th><th>title</th><th>speaker</th><th>affiliation</th><th>slides</th><th>recording</th></tr></thead><tbody><tr><td>09:00</td><td>A Compositional Strategy for Verifying Fault-Tolerant Dynamic Task Graph Scheduling in Modern Cloud Environments</td><td><a href=https://fr.linkedin.com/in/quentin-delamea-380a67198>Quentin Delamea</a></td><td>Aneo & Univ. Saclay</td><td></td><td></td></tr><tr><td>09:30</td><td>A generic hardware in-order pipeline architecture model to capture key temporal properties</td><td><a href=https://www.researchgate.net/profile/Mamoun-Filali>Mamoun Filali</a></td><td>CNRS & IRIT</td><td></td><td></td></tr><tr><td><em>10:00</em></td><td><em>Coffee Break</em></td><td></td><td></td><td></td><td></td></tr><tr><td>10:30</td><td>Extensible Proof Decomposition Rules for TLAPS</td><td><a href=https://www.researchgate.net/profile/Karolis-Petrauskas>Karolis Petrauskas</a></td><td>Vilnius University</td><td></td><td></td></tr><tr><td>11:00</td><td>Systematic API Testing through Model Checking and Executable Contracts</td><td><a href=https://pt.linkedin.com/in/acm-ribeiro>Ana Catarina Ribeiro</a></td><td>NOVA University, Lisbon</td><td></td><td></td></tr><tr><td>11:30</td><td>Model-based Testing of Practical Distributed Systems in Actor Model</td><td><a href=https://www.linkedin.com/in/ilyambda/>Ilya Kokorin</a></td><td>ITMO University</td><td><a href=https://docs.google.com/presentation/d/18oOpSkNoEdvN4Gb8JwrgjM3AFlQTk0JxCoEsRlShZGE/edit>slides</a></td><td></td></tr><tr><td>12:00</td><td>Interactive symbolic testing with TLA+, Apalache, and LLMs</td><td><a href=https://konnov.phd>Igor Konnov</a></td><td></td><td></td><td></td></tr><tr><td><em>12:30</em></td><td><em>Lunch Break</em></td><td></td><td></td><td></td><td></td></tr><tr><td>14:00</td><td>Thinking in TLA+ – Modeling Judgment for System Design</td><td><a href=https://muratbuffalo.blogspot.com>Murat Demirbas</a></td><td>MongoDB</td><td></td><td></td></tr><tr><td>14:50</td><td>P2P2P (PlusCal to PlantUML to PDF)</td><td><a href=https://www.linkedin.com/in/juan-jos%C3%A9-serrano-mora/>Juan José Serrano Mora</a></td><td>Northern Arizona University</td><td></td><td></td></tr><tr><td>15:20</td><td>Towards Language Model Guided TLA+ Proof Automation</td><td><a href=https://www.khoury.northeastern.edu/home/yuhaoz/index.html>Yuhao Zhou</a></td><td>Northeastern University</td><td></td><td></td></tr><tr><td><em>16:00</em></td><td><em>Coffee Break</em></td><td></td><td></td><td></td><td></td></tr><tr><td>16:30</td><td>Verifying differential privacy in TLA+ via self-products</td><td><a href=https://uguryav.uz>Ugur Yavuz</a></td><td>Boston University</td><td></td><td></td></tr><tr><td>17:00</td><td>Veil: Multi-Modal Verification of Transition Systems</td><td><a href=https://pirlea.net>George Pîrlea</a></td><td>National University of Singapore</td><td></td><td></td></tr><tr><td>17:30</td><td>Roundtable & closing</td><td></td><td></td><td></td><td></td></tr><tr><td>19:30</td><td>Workshop dinner</td><td></td><td></td><td></td><td></td></tr></tbody></table><p>Participants are required to <a href=https://etaps.org/2026/registration/>register</a> to ETAPS 2026 (early registration deadline: March 10, 2026).
5+
<span class=links><a href=/>TLA+ Community Event & Conference</a> > 2026 - TLA+ Community Event</span></div><div class=progress><div class=wrapper><nav id=TableOfContents><ul><li><ul><li><a href=#co-located-with-etaps-2026httpsetapsorg2026-in-torino-italy-on-april-12-2026>Co-located with <a href=https://etaps.org/2026/>ETAPS 2026</a> in Torino, Italy, on April 12, 2026.</a></li><li><a href=#schedule>Schedule</a></li><li><a href=#call-for-presentations>Call for presentations</a></li><li><a href=#organizers>Organizers</a></li></ul></li></ul></nav></div></div></div></div><div id=body-inner><div align=right><h4><p>TLA<sup>+</sup> Community Event 2026<br>Sunday, April 12, 2026<br>Torino, Italy<br></p></h4></div><h1 id=tla-community-event-2026>TLA+ Community Event 2026</h1><h3 id=co-located-with-etaps-2026httpsetapsorg2026-in-torino-italy-on-april-12-2026>Co-located with <a href=https://etaps.org/2026/>ETAPS 2026</a> in Torino, Italy, on April 12, 2026.</h3><h3 id=schedule>Schedule</h3><table><thead><tr><th>time</th><th>title</th><th>speaker</th><th>affiliation</th><th>slides</th><th>recording</th></tr></thead><tbody><tr><td>09:00</td><td>A Compositional Strategy for Verifying Fault-Tolerant Dynamic Task Graph Scheduling in Modern Cloud Environments</td><td><a href=https://fr.linkedin.com/in/quentin-delamea-380a67198>Quentin Delamea</a></td><td>Aneo & Univ. Saclay</td><td></td><td></td></tr><tr><td>09:30</td><td>A generic hardware in-order pipeline architecture model to capture key temporal properties</td><td><a href=https://www.researchgate.net/profile/Mamoun-Filali>Mamoun Filali</a></td><td>CNRS & IRIT</td><td></td><td></td></tr><tr><td><em>10:00</em></td><td><em>Coffee Break</em></td><td></td><td></td><td></td><td></td></tr><tr><td>10:30</td><td>Extensible Proof Decomposition Rules for TLAPS</td><td><a href=https://www.researchgate.net/profile/Karolis-Petrauskas>Karolis Petrauskas</a></td><td>Vilnius University</td><td><a href=petrauskas-2026.pdf>slides</a></td><td></td></tr><tr><td>11:00</td><td>Systematic API Testing through Model Checking and Executable Contracts</td><td><a href=https://pt.linkedin.com/in/acm-ribeiro>Ana Catarina Ribeiro</a></td><td>NOVA University, Lisbon</td><td></td><td></td></tr><tr><td>11:30</td><td>Model-based Testing of Practical Distributed Systems in Actor Model</td><td><a href=https://www.linkedin.com/in/ilyambda/>Ilya Kokorin</a></td><td>ITMO University</td><td><a href=kokorin-2026.pdf>slides</a></td><td></td></tr><tr><td>12:00</td><td>Interactive symbolic testing with TLA+, Apalache, and LLMs</td><td><a href=https://konnov.phd>Igor Konnov</a></td><td><a href=konnov-2026.pdf>slides</a></td><td></td><td></td></tr><tr><td><em>12:30</em></td><td><em>Lunch Break</em></td><td></td><td></td><td></td><td></td></tr><tr><td>14:00</td><td>Thinking in TLA+ – Modeling Judgment for System Design</td><td><a href=https://muratbuffalo.blogspot.com>Murat Demirbas</a></td><td>MongoDB</td><td><a href=demirbas-2026.pdf>slides</a></td><td></td></tr><tr><td>14:50</td><td>P2P2P (PlusCal to PlantUML to PDF)</td><td><a href=https://www.linkedin.com/in/juan-jos%C3%A9-serrano-mora/>Juan José Serrano Mora</a></td><td>Northern Arizona University</td><td></td><td></td></tr><tr><td>15:20</td><td>Towards Language Model Guided TLA+ Proof Automation</td><td><a href=https://www.khoury.northeastern.edu/home/yuhaoz/index.html>Yuhao Zhou</a></td><td>Northeastern University</td><td></td><td></td></tr><tr><td><em>16:00</em></td><td><em>Coffee Break</em></td><td></td><td></td><td></td><td></td></tr><tr><td>16:30</td><td>Verifying differential privacy in TLA+ via self-products</td><td><a href=https://uguryav.uz>Ugur Yavuz</a></td><td>Boston University</td><td><a href=yavuz-2026.pdf>slides</a></td><td></td></tr><tr><td>17:00</td><td>Veil: Multi-Modal Verification of Transition Systems</td><td><a href=https://pirlea.net>George Pîrlea</a></td><td>National University of Singapore</td><td><a href=pirlea-2026.pdf>slides</a></td><td></td></tr><tr><td>17:30</td><td>Roundtable & closing</td><td></td><td></td><td></td><td></td></tr><tr><td>19:30</td><td>Workshop dinner</td><td></td><td></td><td></td><td></td></tr></tbody></table><p>Participants are required to <a href=https://etaps.org/2026/registration/>register</a> to ETAPS 2026 (early registration deadline: March 10, 2026).
66
We encourage participants to include the workshop dinner on Sunday evening in their registration.</p><p>Registered participants who cannot attend the meeting in Torino may participate
77
<a href="https://zoom-lfx.platform.linuxfoundation.org/meeting/92459583553?password=caee8799-8e64-42b6-b93e-c767d48c32c4">remotely</a>.</p><h3 id=call-for-presentations>Call for presentations</h3><p><a href=https://lamport.azurewebsites.net/tla/tla.html>TLA+</a> is a language that
88
is used in academia and industry for formally specifying systems. It is

2026-etaps/kokorin-2026.pdf

3.94 MB
Binary file not shown.

2026-etaps/konnov-2026.pdf

4.65 MB
Binary file not shown.

2026-etaps/pirlea-2026.pdf

7.63 MB
Binary file not shown.

2026-etaps/yavuz-2026.pdf

213 KB
Binary file not shown.

0 commit comments

Comments
 (0)