@Article{	  basin.ea:z:2007,
  abstract	= {Z is a standardized and well-established formal
		  specification language originally developed in the 80ies by
		  researchers at oxford University. Although the original
		  emphasis of Z is on specification, the semantics for Z can
		  be expressed within higher-order logic (HOL). On this
		  basis, a theorem-proving environment such as Isabelle/HOL-Z
		  can be built. In this paper, we show how properties over
		  specifications can be formally proven in HOL-Z. Particular
		  emphasis is put on proving relationships between
		  specification such as refinement.},
  author	= {David Basin and Hironobu Kuruma and Shin Nakajima and
		  Burkhart Wolff},
  journal	= {Computer Software --- Journal of the Japanese Society for
		  Software Science and Technology},
  language	= {USenglish},
  month		= {April},
  note		= {In Japanese. },
  number	= 2,
  pages		= {21--26},
  title		= {The Z Specification Language and the Proof Environment
		  Isabelle/HOL-Z},
  volume	= 24,
  year		= 2007,
  user		= {wolff}
}