In early December 2024, the AUTOSARD project launched its activities with a five-day kick-off workshop at the Universitätszentrum Obergurgl. Participants gathered to explore foundational topics in amortised cost analyses, exchange ideas, and build the collaborative spirit that has shaped the project’s first year.
One year later, the project has reached an important milestone: its mid-term phase. To take stock of progress, refine goals, and plan the next stages of research, the AUTOSARD Mid-Term Project Workshop will take place December 8–12, 2025, again at the Universitätszentrum Obergurgl. The workshop will bring together project members and invited researchers to discuss advances, evaluate intermediate results, and strengthen collaborations across teams.
Continuing the tradition of combining intensive research exchange with an inspiring mountain environment, the mid-term workshop will serve as a key moment to assess the path ahead and further shape the project’s long-term impact.
Organizer
Moser, Georg
University of Innsbruck
Participants
Atkey, Robert
University of Strathclyde
Frontull, Samuel
University of Innsbruck
Goetzke, Sven
University of Innsbruck
Hetzenberger, Matthias
TU Wien
Lorenzen, Anton
University of Edinburgh
Moser, Georg
University of Innsbruck
Schaper, Michael
University of Innsbruck
Walch, Armin
University of Innsbruck
Žilinčík, Richard
TU Wien
Zuleger, Florian
TU Wien
AUTOSARD Mid-Term Workshop 2025
Schedule
| Time | Topic | Presenter |
|---|---|---|
| 15:00 | Opening and Welcome | Georg |
| 16:00 | AUTOSARD: Milestones & Ongoing Work | Georg |
| Time | Topic | Presenter |
|---|---|---|
| 08:30 | Automated Amostised Analysis of Leftist Heaps | Armin |
| 09:30 | An Introduction to Refinement Types | Florian |
| 16:00 | Automating Cost Analysis for Quantum Programs | Michael |
| 17:00 | Qurts: Automated Quantum Computation | Sven |
| Time | Topic | Presenter |
|---|---|---|
| 08:30 | Data-Driven Resource Analysis for Functional Programs | Samuel |
| 09:30 | Semantic Cut Elimination | Robert |
| 17:00 | Tutorial on Dependent Types | Robert |
| Time | Topic | Presenter |
|---|---|---|
| 08:30 | Reasoning about First-Order Lazyness | Anton |
| 09:30 | tba | Richard |
| 16:00 | Formal Verification of Zip Trees | Matthias |
| 17:00 | Open Problems | - |
Closing comments and departure.
In the mornings and evenings, participants will hold talks and give presentations about their areas of expertise, while the afternoons will be dedicated to discussions; conversations that will likely continue even on the ski lifts.
We would like to express our sincere gratitude to all participants and project sponsors for contributing to the project’s successful first year, and to the team at the Universitätszentrum Obergurgl for hosting the upcoming workshop.




