# HOL-Z

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 type-checked 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.

## Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

## References in zbMATH (referenced in 11 articles , 1 standard article )

Showing results 1 to 11 of 11.
Sorted by year (citations)

Further publications can be found at: http://www.brucker.ch/projects/hol-z/#bib