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:

Start of Project: October 1, 2013

Members
  • Stéphane Gimenez
  • Andreas Kochesser
  • Georg Moser
  • David Obwaller
  • Thomas Powell
  • Michael Schaper
  • Maria Schett
  • Manuel Schneckenreither
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.
Nach oben scrollen