Alpha: A Tool for Alpha Avoid­ance

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: Auto­mated Amor­tised Com­plex­ity Anal­y­sis of Self-Adjust­ing Data Struc­tures

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.


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.

Tradu­tur Ladin

Webtool for the machine translation of Ladin (Val Badia). This tool gives you the opportunity to test the latest version of the translation tool and to experience the results of ongoing research.

Nach oben scrollen