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