C. Bolton (2005):
Using the Alloy Analyzer to Verify Data Refinement in Z.
Electronic Notes in Theoretical Computer Science 137(2),
pp. 23–44,
doi:10.1016/j.entcs.2005.04.023.
Randal E. Bryant (1986):
Graph-Based Algorithms for Boolean Function Manipulation.
IEEE Trans. Computers 35(8),
pp. 677–691.
Randal E. Bryant (1992):
Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams.
ACM Comput. Surv. 24(3),
pp. 293–318.
E. Clarke, O. Grumberg & D. Peled (2000):
Model Checking.
MIT Press.
W.-P. de Roever & K. Engelhardt (1998):
Data Refinement: Model-Oriented Proof Methods and their Comparison.
CUP,
doi:10.1017/CBO9780511663079.
J. Derrick & E. Boiten (2001):
Refinement in Z and Object-Z, Foundations and Advanced Applications.
Springer-Verlag,
doi:10.1007/978-1-4471-0257-1.
J. Derrick & E.A. Boiten (2003):
Relational Concurrent Refinement.
Formal Aspects of Computing 15(2-3),
pp. 182–214,
doi:10.1007/s00165-003-0007-4.
J. Derrick, S. North & A.J. H. Simons (2008):
Z2SAL - Building a Model Checker for Z.
In: E. Börger, M.J. Butler, J.P. Bowen & P. Boca: ABZ,
Lecture Notes in Computer Science 5238.
Springer,
pp. 280–293,
doi:10.1007/978-3-540-87603-8.
J. Derrick, S. North & T. Simons (2006):
Issues in Implementing a Model Checker for Z.
In: Z. Liu & J. He: ICFEM,
Lecture Notes in Computer Science 4260.
Springer,
pp. 678–696,
doi:10.1007/11901433-37.
John Derrick & Graeme Smith (2008):
Using Model Checking to Automatically Find Retrieve Relations.
Electr. Notes Theor. Comput. Sci. 201,
pp. 155–175,
doi:10.1016/j.entcs.2008.02.019.
C. Fischer & H. Wehrheim (1999):
Model-checking CSP-OZ specifications with FDR.
In: K. Araki, A. Galloway & K. Taguchi: International Conference on Integrated Formal Methods (IFM'99).
Springer-Verlag,
pp. 315–334.
J. He (1989):
Process refinement.
In: J. McDermid: The Theory and Practice of Refinement.
Butterworths.
M. Josephs (1988):
A state-based approach to communicating processes.
Distributed Computing 3,
pp. 9–18.
G. Kassel & G. Smith (2001):
Model Checking Object-Z Classes: Some Experiments with FDR.
In: Asia-Pacific Software Engineering Conference (APSEC 2001).
IEEE Computer Society Press.
M. Leuschel & M. Butler (2005):
Automatic Refinement Checking for B.
In: K. Lau & R. Banach: International Conference on Formal Engineering Methods, ICFEM 2005,
LNCS 3785.
Springer-Verlag,
pp. 345–359.
Tim Miller, Leo Freitas, Petra Malik & Mark Utting (2005):
CZT Support for Z Extensions.
In: Judi Romijn, Graeme Smith & Jaco Pol: Integrated Formal Methods, IFM 2005,
LNCS 3771.
Springer-Verlag,
pp. 227–245.
A. Mota & A. Sampaio (2001):
Model-checking CSP-Z: strategy, tool support and industrial application.
Science of Computer Programming 40,
pp. 59–96.
L. de Moura, S. Owre & N. Shankar (2003):
The SAL language manual.
Technical Report SRI-CSL-01-02 (Rev.2).
SRI International.
Daniel Plagge & Michael Leuschel (2007):
Validating Z Specifications using the ProB Animator and Model Checker.
LNCS 4591,
pp. 480–500.
G. Smith & L. Wildman (2005):
Model checking Z specifications using SAL.
In: H. Treharne, S. King, M. Henson & S. Schneider: International Conference of Z and B Users,
LNCS 3455.
Springer-Verlag,
pp. 87–105.
Graeme Smith & John Derrick (2005):
Model Checking Downward Simulations.
Electr. Notes Theor. Comput. Sci. 137(2),
pp. 205–224,
doi:10.1016/j.entcs.2005.04.032.
Graeme Smith & John Derrick (2006):
Verifying data refinements using a model checker.
Formal Asp. Comput. 18(3),
pp. 264–287,
doi:10.1007/s00165-006-0002-7.
eptcs@eptcs.org