You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
| 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
26
+
| 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
27
+
| _10:00_ | *Coffee Break *
28
+
| 10:30 | Extensible Proof Decomposition Rules for TLAPS | [Karolis Petrauskas](https://www.researchgate.net/profile/Karolis-Petrauskas) | Vilnius University
29
+
| 11:00 | Systematic API Testing through Model Checking and Executable Contracts | [Ana Catarina Ribeiro](https://pt.linkedin.com/in/acm-ribeiro) | NOVA University, Lisbon
30
+
| 11:30 | Model-based Testing of Practical Distributed Systems in Actor Model | Ilya Kokorin | ITMO University
31
+
| 12:00 | Interactive symbolic testing with TLA+, Apalache, and LLMs |[Igor Konnov](https://konnov.phd)|
32
+
| _12:30_ | *Lunch Break*
33
+
| 14:00 | Thinking in TLA+ – Modeling Judgment for System Design | [Murat Demirbas](https://muratbuffalo.blogspot.com) | MongoDB
34
+
| 14:50 | P2P2P (PlusCal to PlantUML to PDF) | [Jackson Belzer](https://www.linkedin.com/in/jackson-belzer) | Northern Arizona University
35
+
| 15:20 | Towards Language Model Guided TLA+ Proof Automation | [Yuhao Zhou](https://www.khoury.northeastern.edu/home/yuhaoz/index.html) | Northeastern University
36
+
| _16:00_ | *Coffee Break*
37
+
| 16:30 | Verifying differential privacy in TLA+ via self-products | [Ugur Yavuz](https://uguryav.uz) | Boston University
38
+
| 17:00 | Roundtable & closing
39
+
| 19:30 | Workshop dinner
40
+
41
+
42
+
Participants are required to [register](https://etaps.org/2026/registration/) to ETAPS 2026 (early registration deadline: March 10, 2026).
43
+
We encourage participants to include the workshop dinner on Sunday evening in their registration.
21
44
22
-
### Accepted presentations
23
-
24
-
* J. Belzer, J.J. Serrano Mora, A.B. Marcos, C. Lamb: P2P2P (PlusCal to PlantUML to PDF)
25
-
* J.-P. Bodeveix, A. Bonenfant, T. Carle, M. Filali, C. Rochange, L. Sylvestre:
26
-
A generic hardware in-order pipeline architecture model to capture key temporal properties
27
-
* Q. Delamea, J. Burman, J. Gurhem, S. Vialle:
28
-
A Compositional Strategy for Verifying Fault-Tolerant Dynamic Task Graph Scheduling in Modern Cloud Environments
29
-
* M. Demirbas: Thinking in TLA+ – Modeling Judgment for System Design
30
-
* I. Kokorin, E. Chernatskiy, V. Aksenov:
31
-
Model-based Testing of Practical Distributed Systems in Actor Model
32
-
* I. Konnov: Interactive symbolic testing with TLA+, Apalache, and LLMs
33
-
* K. Petrauskas: Extensible Proof Decomposition Rules for TLAPS
34
-
* A.C. Ribeiro, M. Mamede, C. Ferreira:
35
-
Systematic API Testing through Model Checking and Executable Contracts
36
-
* U. Yavuz: Verifying differential privacy in TLA+ via self-products
37
-
* Y. Zhou, S. Tripakis: Towards Language Model Guided TLA+ Proof Automation
38
45
39
46
40
47
### Call for presentations
@@ -64,9 +71,6 @@ Proposed contributions should be submitted by January 31, 2026 to tla2026@inria.
64
71
It is expected that the contribution will be presented on 1-2 pages.
65
72
Longer submissions will be read at the discretion of the program committee.
66
73
67
-
Participants will be required to [register](https://etaps.org/2026/registration/) to ETAPS 2026 (early registration deadline: March 10, 2026).
68
-
We encourage participants to include the workshop dinner on Sunday evening in their registration.
69
-
70
74
### Organizers
71
75
* Igor Konnov, researcher in security and formal methods and TU Wien
0 commit comments