Universität Bremen  
  FB 3  
  Group BKB > Research > Formal Methods > Deutsch
English
 

Isabelle@AG BKB
 

Tool Support by Theorem Proving

Formal methods are only viable if supported by appropriate tools. We have found the generic theorem prover Isabelle an excellent means to this end. It is generic, so we can embed our favourite logics or specification languages into it. It is very flexible and powerful, and its source code is available, so we can graft our own extensions onto it.

Isabelle Encodings

Over the years, a couple of embeddings of specification languages have been developed in Bremen. Some of these have now moved elsewhere under the auspices of their authors:
  • HOL-CASL is an embedding of the algebraic specification language CASL into Isabelle/HOL, developed by Till Mossakowski.
  • HOL-CSP is an embedding of the process algebra CSP into Isabelle/HOL, developed by Haykal Tej and Burkhart Wolff.
  • HOL-Z is a structure-preserving embedding of the specification language Z into Isabelle/HOL, originally developed by Kolyang, Thomas Santen and Burkhart Wolff, now in its Version 2.0.
  • The transformational development system TAS allows transformational proof and development in Isbelle, developed by Christoph Lüth and Burkhart Wolff.
Other extensions to Isabelle include the graphical user interface IsaWin. 		 
   
Author: Dr. Christoph Lüth 		 
  Group BKB 
Last updated: September 9, 2002   impressum