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:

- Licence : GPL

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

  WOLFF Burkhart

  Verification of Algorithms, Languages and Systems
Software & patents
The C++ Bulk Synchronous Parallelism Library

A prototype to automate semantic mappings between taxonomies

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