Theoretical Computer Science

Selected Invited Talks

Formal Methods for Quantum Programs
Colloquium of the Theoretical Physics Group at the University of Innsbruck, 23 March 2022, online.

Automated Analysis of Splaying et al.
Seminar on Semantic and Formal Approaches to Complexity (SCOT), 20 January 2021, online.

Resource-Aware Programming ... or what can we learn from Spectre and Meltdown
Shonan Village research seminar Higher-Order Complexity and Its Applications, October 7-10, 2019 in Kanagawa, Japan.

The Epsilon Calculus I
Summer school course at the First International Summerschool for Proof Theory of First-Order Logic in Funchal, Madeira, 2017.

Uniform Resource Analysis by Rewriting: Strengths and Weaknesses
Invited talk at the 2nd FSCD in September, 2017. University of Oxford, UK.

The Epsilon Theorems: Simple Things Made Simple
Workshop on Efficient and Natural Proof Systems, Dec. 16, 2015, University of Bath, UK.

Termination and Complexity
8th International School on Rewriting (ISR 2015), August 13 – 18, HTWK Leipzig, Germany.

Why Ordinals are Good for You
15th European Summer School in Logic Language and Information (ESSLLI 2003), August 18--29, 2003, Vienna, Austria

Selected Publications and Technical Reports

Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
Lorenz Leutgeb, Georg Moser, Florian Zuleger
Proceedings of 34rd Computer Aided Verification, pages 70--91, 2022

Quantum Expectation Transformers for Cost Analysis
Martin Avanzini, Georg Moser, Romain Péchoux, Simon Perdrix, Vladimir Zamdzhiev
Proceedings of 37th LICS, pages 10:1--10:13, 2022

ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures
Lorenz Leutgeb, Georg Moser, Florian Zuleger
Proceedings of 33rd Computer Aided Verification, pp 99-122, 2021

A Modular Cost Analysis for Probabilistic Program
Martin Avanzini, Georg Moser, Michael Schaper
Proceedings of the ACM on Programming Languages, Volume 4, Issue OOPSLA, November 2020, Article No.: 172, pp 1–30

Resource Analysis of Imperative Programs
Michael Schaper, PhD thesis, University of Innsbruck, 2020.

Automated Amortised Resource Analysis for Term Rewrite Systems
Georg Moser, Manuel Schneckenreither
Sci. Comput. Program. 185 (2020)

From Jinja Bytecode to Term Rewriting: A Complexity Reflecting Transformation
Georg Moser and Michael Schaper, Inf. Comput. 261(Part): 116-143 (2018)

KBOs, ordinals, subrecursive hierarchies and all that
Georg Moser, J. Log. Comput. 27(2): 469-495 (2017)

The Complexity of Interaction
Stéphane Gimenez and Georg Moser, 43rd POPL, 2016.

Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order
Martin Avanzini, Ugo Dal Lago, and Georg Moser, 20th ICFP, 2015.

Multivariate Amortised Resource Analysis for Term Rewrite Systems
Martin Hofmann, Georg Moser, 13th TLCA, 2015.

A Combination Framework for Complexity
Martin Avanzini, Georg Moser, special issue of IC, 2016.

A New Order-theoretic Characterisation of the Polytime Computable Functions
Martin Avanzini, Naohi Eguchi, Georg Moser, special issue of TCS, 2015.

Verifying Polytime Computability Automatically
Martin Avanzini, PhD thesis, University of Innsbruck, 2013.

Derivational Complexity Analysis Revisited
Andreas Schnabl, PhD thesis, University of Innsbruck, 2012.

Proof Theory at Work: Complexity Analysis of Term Rewrite Systems
Georg Moser, CoRR abs/0907.5527 (2009)

Further publications of the group can partially also be found here.