TAS and IsaWin home page.

Welcome to the TAS and IsaWin home page!

[Glimpse

TAS and IsaWin are tools for formal program development and theorem proving developed at the University of Bremen and Albert-Ludwigs-Universität, Freiburg.

TAS is a transformation system based on the theorem prover Isabelle. It features:

In particular, genericity means it can be used for any formal method which offers a notion of correctness-preserving refinement, or in fact any transitive-reflexive transformation relation, which is encoded into Isabelle. We have investigated instantiations for classical program transformations (in the style of systems like KIDS using plain higher-order logic), for the specification language Z (using the HOL-Z encoding), the process calculus CSP (using the HOL-CSP encoding), and the algebraic specification language CASL (using the HOL-CASL encoding).

IsaWin is a graphical user interface for the theorem prover Isabelle. It offers the user a more abstract view on Isabelle then its ususal command-line based interface.

Both systems are built using sml_tk, an encapsulation of the user interface description language and library Tcl/Tk into Standard ML (SML). Building on this, we provide a Generic Interface Toolkit which can be used to quickly built graphical user interfaces like TAS and IsaWin.

Demos and Screenshots

Here is a full screenshot of TAS and IsaWin, but you to get a taste of TAS and IsaWin you can download a demo version below. Note that these are preliminary demo versions with a deliberately limited functionality. The demos are plug&play without a complicated configuration procedure. To run them, unpack the file tas_demo.tar.gz. This will produce a directory tas_demo. Go into this directory, and call bin/TAS_demo. The file README (in tas_demo) contains further information.

TAS and IsaWin are still in a prototypical stage, so we unfortunately at this point we can only make the demo versions above available to the public. A full working version should be available by the start of the next year.

Papers and Documentation

Here are a couple of papers about TAS and IsaWin. More can be found here and here. On a more historic note, the system YATS, the ancestor of TAS from which it inherits its design and many concepts, is described in:

Personnel

TAS, IsaWin and the Generic Interface Toolkit are developed jointly by Christoph Lüth at the University of Bremen and Burkhart Wolff at the Albert-Ludwigs-Universität Freiburg. The development was initially funded by the UniForM project.
Christoph Lüth. Last modified: Tue Dec 2 16:09:09 CET 2003