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

Le Système HOL-Z - The HOL-Z System
Date of the last release: 16 June 2008

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:

Software - Licence : GPL

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

  WOLFF Burkhart

  Verification of Algorithms, Languages and Systems

Software & patents

Deep Neural Architectures for DNA