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.

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

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

  1. Cavalcanti, Ana; Gaudel, Marie-Claude: Testing for refinement in \textsfCircus (2011)
  2. Jackson, Ethan; Sztipanovits, Janos: Formalizing the structural semantics of domain-specific modeling languages (2009) ioport
  3. Brucker, Achim D.; Wolff, Burkhart: An extensible encoding of object-oriented data models in HOL. With an application to IMP++ (2008)
  4. Brucker, Achim D.; Wolff, Burkhart: Extensible universes for object-oriented data models (2008) ioport
  5. Basin, David; Kuruma, Hironobu; Miyazaki, Kunihiko; Takaragi, Kazuo; Wolff, Burkhart: Verifying a signature architecture: a comparative case study (2007)
  6. Pretschner, Alexander; Prenninger, Wolfgang: Computing refactorings of state machines (2007) ioport
  7. Wenzel, Makarius; Wolff, Burkhart: Building formal method tools in the Isabelle/Isar framework (2007)
  8. Basin, David; Kuruma, Hironobu; Takaragi, Kazuo; Wolff, Burkhart: Verification of a signature architecture with HOL-Z (2005)
  9. Brucker, Achim D.; Wolff, Burkhart: A verification approach to applied system security (2005) ioport
  10. Brucker, Achim D.; Wolff, Burkhart: A verification approach to applied system security (2005) ioport
  11. Brucker, A. D.; Rittinger, F.; Wolff, B.: Hol-z 2.0: a proof environment for z-specifications (2003) ioport

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