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.

Eco-imp and Ev-imp

Eco-imp performs an expected cost analysis for simple imperative programs, in the style of Dijkstra's Guarded Command Language, featuring probabilistic sampling instructions, while ev-imp provides a fully automated expected value analysis of similar non-deterministic, probabilistic imperative programs. However, in the presence of natural programming constructs such as procedures, local variables and recursion. Noteworthy, ev-imp is not restricted to tail-recursion, which could unarguably be replaced by iteration and wouldn't need additional insights.

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.