More About TAS and IsaWin - Tools for Formal Program Development

We present a family of tools for program development and verification, comprising the transformation system TAS and the theorem proving interface IsaWin. Both are based on the theorem prover Isabelle [8], which is used as a generic logical framework here. A graphical user interface, based on the principle of direct manipulation, allows the user to interact with the tool without having to concern himself with the details of the representation within the theorem prover, leaving him to concentrate on the main design decisions of program development or theorem proving.

• Type: Conference
• Year: 2000
• Where: FASE
• Authors: Christoph Lüth, Burkhart Wolff
• Keywords: FASE 2000, Software Engineering, Theorem Prover, Theorem Proving, Theorem Proving Interface