Several projects resulted in software products that can be obtained under
freeware conditions for non-profit use. Please consult the COPYRIGHT licenses
in each case.
is a visualization tool for directed graphs.
sml_tk is a typed encapsulation of Tcl/Tk into
Standard ML, to conveniently build graphical user interfaces for SML applications.
HOL-CSP is a conservative embedding of the
failure-divergence modell for CSP into Isabelle/HOL.
HOL-Z is a shallow, structure-preserving embedding
of Z into Isabelle/HOL.
IsaWin are tools for transformational
program development and verification, based on Isabelle.
CATS is a tool set
for processing CASL
HOL-CASL is a tool for
theorem proving with CASL specifications, based on Isabelle and IsaWin.
Hets, the Heterogeneous tool set,
can parse and statically analyse HetCASL,
a heterogeneous specification language. Hets also supports
heterogeneous theorem proving.