C-SHORe, Collapse-Saturation for Higher-Order Recursion, a new tool to automatically check termination (or related properties) of functional programs.

ACME, ACME is a tool implementing algebraic techniques to solve decision problems from automata theory. The core generic algorithm takes as input an automaton and computes its stabilization monoid, which is a generalization of its transition monoid.

cpaut, Sage package to test and display algebraic properties on regular languages.