Assoc. Prof. Dr. Georg Moser   

Termination

T. Arts and J. Giesl.
Termination of Term Rewriting using Dependency Pairs.
TCS, 236(1,2):133--178, 2000.

C.S. Lee, N.N. Jones, A.M. Ben-Amram.
The size-change principle for program termination.
In Proc. POPL, pages 81-92, 2001.

J. Endrullis, J. Waldmann, and H. Zantema.
Matrix Interpretations for Proving Termination of Term Rewriting.
JAR, 40(3):195--220, 2008.

A. Geser, D. Hofbauer, J. Waldmann, and H. Zantema.
On Tree Automata that Certify Termination of Left-Linear Term Rewriting Systems.
IC, 205(4):512--534, 2007.

J. Giesl, R. Thiemann, and P. Schneider-Kamp.
The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs.
In Proc. of 11th LPAR, pages 301--331, 2005.

N. Hirokawa and A. Middeldorp.
Automating the Dependency Pair Method.
IC, 199(1,2):172--199, 2005.

N. Hirokawa and A. Middeldorp.
Tyrolean Termination Tool: Techniques and Features.
IC, 205:474--511, 2007.

R. Thiemann.
The DP Framework for Proving Termination of Term Rewriting.
PhD thesis, University of Aachen, 2007.

Derivational Complexity Analysis

D. Hofbauer and C. Lautemann.
Termination proofs and the length of derivations.
In Proc. 3rd RTA, pages 167--177, 1989.

D. Hofbauer.
Termination Proofs with Multiset Path Orderings Imply Primitive Recursive Derivation Lengths.
TCS, 105(1):129--140, 1992.

G. Moser and A. Weiermann.
Relating Derivation Lengths with the Slow-Growing Hierarchy Directly.
In Proc. of 14th RTA, pages 296-310, 2003.

A. Middeldorp, G. Moser, F. Neurauter, J. Waldmann, and H. Zankl.
Joint spectral radius theory for automated complexity analysis of rewrite systems.
In Proc. 4th CAI, pages 1­20, 2011.

G. Moser and A. Schnabl.
The Derivational Complexity Induced by the Dependency Pair Method.
Logical Methods in Computer Science 7(3:1), pp. 1 – 38, 2011.

G. Moser and A. Schnabl.
Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity.
In Proc. 22nd RTA, pages 235 – 250, 2011.

G. Moser and T. Powell.
On the Computational Content of Termination Proofs.
In Proc. 11th CiE, pages 276-285, 2015.

A. Schnabl
University of Innsbruck.
PhD thesis, Derivational Complexity Analysis revisited, 2012.

J. Waldmann.
Polynomially Bounded Matrix Interpretations.
In Proc. of. 21th RTA, pages 357-372, 2010.

Runtime Complexity Analysis

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

M. Avanzini, N. Eguchi, and G. Moser
A new Order-theoretic Characterisation of the Polytime Computable Functions.
Theoretical Computer Science 585:3-24, 2015. Elsevier.

M. Avanzini, N. Eguchi, and G. Moser
A Path Order for Rewrite Systems that Compute Exponential Time Functions.
In Proc. 22nd RTA, pages 123 – 138, 2011.

G. Bonfante, A. Cichon, J. Marion, and H. Touzet.
Algorithms with Polynomial Interpretation Termination Proof.
Journal of Functional Programming, 11(1), pages 33--53, 2001.

N. Hirokawa and G. Moser.
Automated Complexity Analysis Based on the Dependency Pair Method.
In Proc. of. 4th IJCAR, pages 364--379, 2008.

N. Hirokawa and G. Moser.
Complexity, Graphs, and the Dependency Pair Method.
In Proc. of. 15th LPAR, pages 652--666, 2008.

L. Noschinski, F. Emmes, and J. Giesl.
Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs.
J. Autom. Reasoning 51(1): 27-56, 2013.

Program Analysis and Implicit Computational Complexity

R. Atkey.
Amortised Resource Analysis with Separation Logic
Logical Methods in Computer Science 7(2), 2011.

M. Avanzini, U. Dal Lago, G. Moser
Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order
In Proc. 20th ICFP, 2015.

M. Avanzini and G. Moser.
Closing the Gap Between Runtime Complexity and Polytime Computability.
In Proc. of. 21th RTA, 2010.

A.M. Ben-Amram and S. Genaim.
Ranking Functions for Linear-Constraint Loops.
J. ACM 61(4) 26, pages 1-26:55, 2014.

G. Bonfante and G. Moser.
Characterising Space Complexity Classes via Knuth-Bendix orders.
In Proc. 17th LPAR, ArCoS, 2010.

T. Colcombet, L. Daviaud, and F. Zuleger.
Size-Change Abstraction and Max-Plus Automata.
In Proc. 39 MFCS, pages 208-219, 2014.

J. Hoffmann, K. Aehlig, and M. Hofmann.
Multivariate amortized resource analysis.
In Proc. POPL'11, pages 357­– 369, 2011.

J.-Y. Marion.
Analysing the Implicit Complexity of Programs.
IC, 183:2--18, 2003.

M. Sinn, F. Zuleger, and H. Veith.
A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis.
In Proc. CAV, pages 745-761, 2014.