Theoretical Computer Science

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 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 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.


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


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.