**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