@Article{ brucker.ea:hol-z:2003,
abstract = {We present a new proof environment for the specification language Z. The basis is a semantic
representation of Z in a structure-preserving, shallow embedding in Isabelle/HOL. On top of the
embedding, new proof support for the Z schema calculus and for proof structuring are developed. Thus,
we integrate Z into a well-known and trusted theorem prover with advanced deduction technology such as
higher-order rewriting, tableaux-based provers and arithmetic decision procedures. A further
achievement of this work is the integration of our embedding into a new tool-chain providing a
Z-oriented type checker, documentation facilities and macro support for refinement proofs; as a
result, the gap has been closed between a logical embedding proven correct and a \emph{tool} suited
for applications of non-trivial size.},
author = {Achim D. Brucker and Frank Rittinger and Burkhart Wolff},
journal = {Journal of Universal Computer Science},
language = {USenglish},
title = {{HOL}-{Z} 2.0: {A} Proof Environment for {Z}-Specifications},
volume = {9},
number = {2},
pages = {152--172},
month = feb,
year = {2003},
pdf = {https://www.brucker.ch/bibliography/download/2003/brucker.ea-hol-z-2003.pdf},
keywords = {Theorem Proving, Refinement, Z},
copyright = {J.UCS},
copyrighturl = {http://www.jucs.org/jucs_9_2/hol_z_2},
categories = {holz},
doi = {10.3217/jucs-009-02-0152},
issn = {0948-6968},
classification= {journal},
areas = {formal methods, software},
public = {yes},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-hol-z-2003}
}