The CZT verification condition generator supports generating conjectures about Z specifications used to verify their correctness and consistency.

The following verification conditions are supported:

  • Domain checks (function application, axiomatic definitions, etc.)
  • Feasibility checks (operation preconditions)
  • Refinement checks (refinement correctness, experimental)

Back to top

Version: 1.6-SNAPSHOT. Last Published: 2016-04-09.

Reflow Maven skin by Andrius Velykis.