Français Anglais
Accueil Annuaire Plan du site
Home > Research results > Software & patents
Research results
Le Système HOL-Z


Le Système HOL-Z - The HOL-Z System


Person in charge : WOLFF Burkhart


HOL-Z is a proof environment for Z built as plug-in of the generic theorem prover Isabelle/HOL (Version 2005). It allows for importing Z specifications written in LaTeX and typechecked by the Java-based ZeTa-System. HOL-Z then allows for the formal analysis of such specifications, i.e. by
proving the conjectures stated in the specfication,
generating proof obligations concerning the consistency
of state and operation schemas as well as their proof, and
generating proof obligations resulting from refinement
statements for functional and data refinement (cf. Spivey`s The Z Reference Manual).

Proof documents containing lemmas, analytical statements, proofs and global checks were written in an extension of the Isabelle/ISAR proof language and can be edited with the emacs-based ProofGeneral 3.6 interface.

More information: http://www.brucker.ch/projects/hol-z/

- Licence : GPL



Research activities
  Formalisation of (Specification and Programming) Languages in Proof Assistants

Members
  WOLFF Burkhart

Group
  Verification of Algorithms, Languages and Systems
Software & patents
TAXOMAP ALIGNMENT
A prototype to automate semantic mappings between taxonomies

BSP++
The C++ Bulk Synchronous Parallelism Library

FR1155729
Procédé pour l’extinction de routeurs dans un réseau de communications et routeur mettant en œuvre ce procédé