TcT - A Complexity Analyser

TcT3 is the latest version of our fully automated complexity analyser. TcT implements a framework for automated complexity analysis and supports various formal systems and programming languages.

It is developed by members of the Computation with Bounded Resources research group. 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.

News

TcT version 3.3 released 2019/05/10 Compatibility release for recent ghc version (ghc-8.6.5).

Automated Amortized Resource Analysis for Term Rewrite Systems 2017/12/01 TcT now supports amortized resource analysis of term rewrite systems (currently only avaialable at the development branch).

TcT version 3.0 released 2015/10/16 TcT version 3.0 was released. It is a complete reimplementation of version 2.0.1, which is open to arbitrary complexity problems and allows seamless integration of 3rd party solvers.

TcT won a Kurt Gödel medal 2014/07/21 In 2014, the first "FLoC Olympic Games" have been conducted during the Vienna Summer of Logic. During the games, several automatic tools competed in 14 different competitions about complexity, determinacy, satisfiablity, termination, etc. TcT competed in the termination competition and won the prize for the most powerful tool in complexity analysis of term rewrite systems.

TcT version 2.0.1 released 2013/08/06 TcT version 2.0.1 has been released. This minor release comes with updated documentation, minor bugfixes, and a more consistent naming of techniques in Tct.Instances.

TcT version 2.0 released 2013/03/19 TcT version 2.0 has been released. Besides bug-fixes and a wealth of minor improvements, notably this release adds to version 1.9: Interactive mode can now exploit multiple cores Simplified configuration. See an example (available also in the source distribution) or the updated documentation A GNU/Emacs mode, available from here

Web Interface Updated 2013/03/01 Our web interface has been polished, it features new examples, the competition strategy of 2012 and a dedicated strategy for our RaML collection.

Complexity Competition 2012 2013/02/02 TcT participated in all four complexity categories of the complexity competition 2012. TcT won the runtime complexity category. It is the only tool participating in the innermost derivational complexity category, and the only open source tool capable of proving innermost runtime complexity. TcT could signifficantly increase its power for innermost runtime complexity, and was placed closely after AProVE (closed source).

Web Interface 2012/05/10 TcT now features an easy to use web interface.

Resource aware ML 2012/05/10 We have translated the Resource aware ML testbed to term rewrite systems. The resulting set of TRSs can be downloaded from here.

TcT version 1.9 released 2012/01/01 This version presents the last milestone before version 2.0. Besides various bugfixes, most notably following new features are added: Improved documentation for using and extending TcT A new interactive interface A new notion of complexity preserving transformations, including a wealth of combinators, c.f. the documentation. Most of the old processors are implemented as transformations now. TcT now features its own xml output-format which can be translated using the provided XSLT stylesheet to CPF. added small polynomial path orders, improved dependency graph decomposition and various simplifications techniques for the (weak) dependency pair setting.

News archive

Contact

TcT is currently under development by Martin Avanzini, Georg Moser and Michael Schaper.
Former developers: Andreas Schnabl, Andreas Kochesser, Maria Schett and Manuel Schneckenreither.