Program
2025-04-02 (Day 1)
9:00–10:30 |
Session 1 |
| 9:00–9:30 |
Zsófia Ádám Towards a 2.0 Non-Termination Witness Format (joint work with Paulína Ayaziová, Levente Bajczi, Dirk Beyer, Marek Jankola, Marian Lingsch-Rosenfeld, and Jan Strejček) |
| 9:30–10:30 |
Discussion (moderated by Dirk Beyer, Jan Strejček and Marian Lingsch-Rosenfeld) |
10:10–10:30 |
Coffee break |
10:30–12:00 |
Session 2 |
| 10:30–11:00 |
Frank Schüssele Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts (joint work with Julian Erhard, Manuel Bentele, Matthias Heizmann, Dominik Klumpp, Simmo Saan, Michael Schwarz, Helmut Seidl, Sarah Tilscher, and Vesal Vojdani) |
| 11:00–12:00 |
Discussion (moderated by Dirk Beyer, Jan Strejček and Marian Lingsch-Rosenfeld) |
12:00–13:00 |
Lunch |
13:00–15:30 |
Session 3 |
| 13:00–13:30 |
Levente Bajczi Violation Witnesses for (Weakly Consistent) Concurrent Programs (joint work with Marian Lingsch-Rosenfeld) |
| 13:30–14:15 |
Discussion (moderated by Dirk Beyer, Jan Strejček and Marian Lingsch-Rosenfeld) |
| 14:15–14:45 |
Marek Jankola Transition Invariants as Building Blocks for Termination Witnesses (joint work with Dirk Beyer, and Marian Lingsch-Rosenfeld) |
| 14:45–15:30 |
Discussion (moderated by Dirk Beyer, Jan Strejček and Marian Lingsch-Rosenfeld) |
15:30–16:00 |
Coffee break |
16:00–18:00 |
Session 4 |
| 16:00–16:30 |
Matthias Heizmann Inductive Witnesses (joint work with Dominik Klumpp, Marian Lingsch-Rosenfeld, Frank Schüssele) |
| 16:30–18:00 |
Discussion (moderated by Dirk Beyer, Jan Strejček and Marian Lingsch-Rosenfeld) |
2025-04-03 (Day 2)
9:00–10:30 |
Session 1 |
| 9:00–9:30 | td> Gidon Ernst|
| 9:30–10:30 |
Discussion (moderated by Dirk Beyer, Jan Strejček and Marian Lingsch-Rosenfeld) |
10:30–11:00 |
Coffee break |
11:00–12:00 |
Session 2 |
| 11:00–12:00 |
Discussion (moderated by Dirk Beyer, Jan Strejček and Marian Lingsch-Rosenfeld) |
12:00–13:00 |
Lunch |
14:00–15:30 |
Session 3 |
| 14:00–15:30 |
Discussion (moderated by Dirk Beyer, Jan Strejček and Marian Lingsch-Rosenfeld) |
15:30–16:00 |
Coffee break |