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

• 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

Contact

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.