### Automated Complexity Analysis via Transformations

This project is concerned with analysing the complexity of programs. This is a highly important subject, since the complexity of a program essentially determines its usefulness. We aim at a tool that performs a static program analysis and that can handle existing programming languages, not only toy languages.The two main goals of the project are

- to obtain
*automated complexity preserving transformations*from Java and Prolog into term rewrite systems (TRSs for short), and - to advance the state of the art of
*automated complexity analysis of term rewrite systems*.

In these goals we seek precise asymptotic polynomial bounds that may be non-linear. Through the abstract representation of programs as rewrite system our analysis enables disjunctive bounds and through the use of a dedicated combination framework we achieve compositionality and thus effectivity of the method.

We summarise the goals of the project as follows: *Advance the state of the art of complexity analysis of programs by investigating automated runtime complexity analysis via transformations.*

#### Duration: 3 years

Start of Project: October 1, 2013

#### Members

- Stéphane Gimenez
- Andreas Kochesser
- Georg Moser
- David Obwaller
- Thomas Powell
- Michael Schaper
- Maria Schett
- Manuel Schneckenreither

h4. Meetings

- Logic, Complexity and Automation, September 5-7, 2016, Obergurgl, Austria
- Two Faces of Complexity 2014, Saturday, July 12, 2014, Vienna, Austria

#### Vacancies

Currently there are no vacancies in the project.

#### FWF “Single Project” project number

P 25781-N15#### Contact

georg.moser@uibk.ac.at#### Publications

Bar Recursion over Finite Partial Functions

Paulo Oliva and Thomas Powell

Annals of Pure and Applied Logic 2016.

Gödel’s Functional Interpretation and the Concept of Learning

Thomas Powell

Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016),
pp. 136 – 145,
2016.

Running Interaction Nets on Random Access Machines

Stephane Gimenez and Georg Moser

Proceedings of the 8th International Workshop on Higher-Order Rewriting (HOR 2016),
2016.

Interaction Automata and the ia2d Interpreter

Stéphane Gimenez and David Obwaller

Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016),
Leibniz International Proceedings in Informatics 52,
pp. 35:1 – 35:11,
2016.

Complexity of Acyclic Term Graph Rewriting

Martin Avanzini and Georg Moser

Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016),
Leibniz International Proceedings in Informatics 52,
pp. 10:1 – 10:18,
2016.

Kruskal’s Tree Theorem for Term Graphs

Georg Moser and Maria A. Schett

Proceedings of the 9th International Workshop on Computing with Terms and Graphs (TERMGRAPH 2016),
2016.

TcT: Tyrolean Complexity Tool

Martin Avanzini, Georg Moser and Michael Schaper

Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016),
Lecture Notes in Computer Science 9636,
pp. 407 – 423,
2016.

The Complexity of Interaction

Stéphane Gimenez and Georg Moser

Proceedings of the 7th Workshop on Developments in Implicit Computational Complexity (DICE 2016),
2016.

The Complexity of Interaction

Stéphane Gimenez and Georg Moser

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016),
243 – 255,
2016.

Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order

Martin Avanzini, Ugo Dal Lago, and Georg Moser

Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015),
pp. 152 – 164,
2015.

Parametrised Bar Recursion: A Unifying Framework for Realizability Interpretations of Classical Dependent Choice

Thomas Powell

Journal of Logic and Computation 2015.

Multivariate Amortised Resource Analysis for Term Rewrite System

Martin Hofmann and Georg Moser

Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015),
Leibniz International Proceedings in Informatics 38,
pp. 241 – 256,
2015.

On the Computational Content of Termination Proofs

Georg Moser and Thomas Powell

Proceedings of the 11th Conference on Computability in Europe (CiE 2015),
Lecture Notes in Computer Science 9136,
pp. 276 – 285,
2015.

Leftmost Outermost Revisited

Nao Hirokawa, Aart Middeldorp, and Georg Moser

Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA 2015),
Leibniz International Proceedings in Informatics 36,
pp. 209 – 222,
2015.

Higher-Order Complexity Analysis: Harnessing First-Order Tools

Martin Avanzini, Ugo Dal Lago and Georg Moser

Proceedings of the 6th Workshop on Developments in Implicit Computational Complexity (DICE 2015),
2015.

Amortised Resource Analysis and Typed Polynomial Interpretations

Martin Hofmann and Georg Moser

Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014),
Lecture Notes in Computer Science 8560,
pp. 272 – 286,
2014.

A Complexity Preserving Transformation from Jinja Bytecode to Rewrite Systems

Georg Moser and Michael Schaper

Presented at the 1st International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2014),
2014.

A Complexity Preserving Transformation from Jinja Bytecode to Rewrite Systems

Michael Schaper

Presented at the 5th Workshop on Developments in Implicit Computational Complexity (DICE 2014),
2014.