Alpha: A Tool for Alpha Avoidance

The alpha avoidance tool provides an automated verification of alpha avoidance in typed and untyped lambda-terms. It is based on the detection of alpha paths, a novel method to completely characterise whether or not alpha conversions are essential in beta reductions.

ATLAS

ATLAS provides a fully automated expected amortised cost analysis of self-adjusting data structures, that is, of randomised splay trees, randomised splay heaps, randomised meldable heaps and other sophisticated data structures (not necessarily randomised), which so far have only (semi-)manually been analysed in the literature.

Ecoimp

Ecoimp provides a fully automated resource analysis of non-deterministic, probabilistic imperative programs, employing a modular approach: program fragments are analysed in full independence. Further, ecoimp incorporates sampling from dynamic distributions, making our analysis applicable to a wide class of examples, for example the Coupon Collector's problem.

Rewriting

The rewriting library for Haskell is jointly developed with other members from the computational logic research group. Sources are availabe from here.

TcT

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.