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: Automated Amortised Complexity Analysis of Self-Adjusting Data Structures
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.
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.
Tradutur 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.