Tyrolean Complexity Tool

The Tyrolean Complexity Tool (TcT for short) is a fully automated resource analysis tool for (i) first-order term rewrite systems; (ii) integer transition systems; (iii) higher-order functional programs; and (iv) object-oriented bytecode programs.

As repeatedly verified by the annual termination competition (TERMCOMP) and at the FLOC Olympic Games 2014, TcT is the most powerful complexity analyser for term rewrite systems and state of the art for higher-order functional programs.

Web Interface

Choose your destiny

• Term Rewrite Systems
• Integer Transition Systems
• Higher-Order Functional Programs
• Object Oriented Bytecode Programs

Versions

TcT version 3.3, released 2019/05/10, is the latest version of our fully automated resource analysis tool. TcT implements a framework for automated complexity analysis and supports various formal systems and programming languages.

The latest version is a reimplementation of the complexity framework that focuses on extensibility and automation. TcT is open with respect to the complexity problem under investigation and problem specific techniques. Moreover it provides an expressive problem independent strategy language that facilitates the proof search.

Download

TcT is hosted on our Github page. It consists of multiple packages. Most likely you want one of tct-its, tct-trs or tct-hoca. The installation procedures and requirements are provided in the README.md file (which is displayed on the respective Github-project page). Following modules are available:

TcT instances:

• tct-its: Automatic complexity analysis tool for integer transition systems
• tct-trs: Automatic complexity analysis tool for term rewrite systems
• tct-hoca: Automatic complexity analysis tool for higher-order systems
• tct-jbc: Automatic complexity analysis tool for Jinja bytecode

Other modules:

• tct-core: Transformation framework for complexity analysis
• tct-common: Common functionalities for TcT
• jat: Transformation from Jinja bytecode to term rewrtite systems
• hoca: Automatic complexity analysis tool for higher-order systems
• term-rewriting-applicative: Applicatives for term-rewriting library
• slogic: A s(imple)logic library providing interfaces to to external solvers
• term-rewriting-xml: XML parser for term-rewriting library

License

The releases are licensed under BSD3. See http://directory.fsf.org/wiki/License:BSD_3Clause for more information on BSD3.

Old releases

The old releases of TcT are still available in our archive.

Contact

TcT is developed by members of the Theoretical Computer Science group.