Timbuk 4 is specialized
for functional program analysis (needs CVC4).
 Targets higherorder functional programs encoded into TRS.
 Proves structural properties on algebraic data
types manipulated by such programs.
 Tree automata proving such properties are built
automatically.
Here is
the source
distribution and
the results
of some experiments on functional program automatic verification.

Timbuk 3.2 generic reachability analysis tool and
tree automata library.
 General purpose tree automata library implementing
all wellknown algorithms.
 Conversion between tree regular expressions and tree
automata, and vice versa (using the algorithms coming from
this paper
and from this one).
 Reachability analysis on TRS using both automatic
and manual definition of approximations.
See below for installation
instructions or use it in your browser . This requires no
installation but takes some time to start!
