Software Publications

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.

• uDraw(Graph) 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.
• TAS and IsaWin are tools for transformational program development and verification, based on Isabelle.
•  CATS is a tool set for processing  CASL specifications.
•  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.