@inproceedings(Ref-Reach:Ev-B:2005,
 author       = "J.R. Abrial and D. Cansell and D. M\'ery",
 year         = "2005",
 title        = "Refinement and Reachability in {E}vent\unhbox \voidb@x \kern 0.06em\vbox {\hrule width0.5em}{B}",
 booktitle    = "ZB2005",
 series       = "LNCS",
 volume       = "3455",
 publisher    = "Springer",
 pages        = "222--241",
 doi          = "10.1007/11415787\unhbox \voidb@x \kern 0.06em\vbox {\hrule width0.5em}14",
)
@phdthesis(PhDThesis,
 author       = "N. Am\'alio",
 year         = "2007",
 title        = "Generative frameworks for rigorous model-driven development",
 school       = "Dept. Computer Science, Univ. of York",
)
@inproceedings(VCL:VCB:2011,
 author       = "N. Am\'alio and C. Glodt and P. Kelsen",
 year         = "2011",
 title        = "Building {VCL} models and automatically generating {Z} specifications from them",
 booktitle    = "FM 2011",
 series       = "LNCS",
 volume       = "6664",
 publisher    = "Springer",
 pages        = "149--153",
 doi          = "10.1007/978-3-642-21437-0\unhbox \voidb@x \kern 0.06em\vbox {\hrule width0.5em}13",
)
@inproceedings(VCL:DBC:2010,
 author       = "N. Am\'alio and P. Kelsen",
 year         = "2010",
 title        = "Modular Design by Contract Visually and Formally using {VCL}",
 booktitle    = "VL/HCC 2010",
 publisher    = "IEEE",
 pages        = "227--234",
 doi          = "10.1109/VLHCC.2010.39",
)
@article(VCL:TAOSD:2010,
 author       = "N. Am\'{a}lio and P. Kelsen and Q. Ma and C. Glodt",
 year         = "2010",
 title        = "Using {VCL} as an Aspect-Oriented Approach to Requirements Modelling",
 journal      = "TAOSD",
 volume       = "VII",
 pages        = "151--199",
 doi          = "10.1007/978-3-642-16086-8\unhbox \voidb@x \kern 0.06em\vbox {\hrule width0.5em}5",
)
@inproceedings(ZOO:2005,
 author       = "N. Am\'{a}lio and F. Polack and S. Stepney",
 year         = "2005",
 title        = "An Object-Oriented Structuring for {Z} based on Views",
 booktitle    = "ZB 2005",
 series       = "LNCS",
 volume       = "3455",
 publisher    = "Springer",
 pages        = "262--278",
 doi          = "10.1007/11415787\unhbox \voidb@x \kern 0.06em\vbox {\hrule width0.5em}16",
)
@inproceedings(Amalio:2006aa,
 author       = "N. Am\'{a}lio and F. Polack and S. Stepney",
 year         = "2006",
 title        = "{UML+Z}: Augmenting {UML} with {Z}",
 editor       = "H. Abrias and M. Frappier",
 booktitle    = "Software Specification Methods",
 publisher    = "ISTE",
 doi          = "10.1002/9780470612514.ch5",
)
@inproceedings(Banach:1998fk,
 author       = "R. Banach and M. Poppleton",
 year         = "1998",
 title        = "Retrenchment: An engineering variation on refinement",
 booktitle    = "B'98",
 series       = "LNCS",
 volume       = "1393",
 publisher    = "Springer",
 pages        = "129--147",
 doi          = "10.1007/BFb0053358",
)
@article(Banach:2007fk,
 author       = "R. Banach and M. Poppleton and C. Jeske and S. Stepney",
 year         = "2007",
 title        = "Engineering and theoretical underpinnings of retrenchment",
 journal      = "Science of Computer Programming",
 volume       = "67",
 number       = "2--3",
 pages        = "301--329",
 doi          = "10.1016/j.scico.2007.04.002",
)
@article(Cardelli:1988uq,
 author       = "L. Cardelli",
 year         = "1988",
 title        = "A semantics of multiple inheritance",
 journal      = "Information and Computation",
 volume       = "76",
 pages        = "138--164",
 doi          = "10.1016/0890-5401(88)90007-7",
)
@book(Refinement-Z-OZ,
 author       = "J. Derrick and E. Boiten",
 year         = "2001",
 title        = "Refinement in {Z} and {O}bject-{Z}: foundations and advanced applications",
 publisher    = "Springer",
)
@inproceedings(Beh-Inh:FW:2000,
 author       = "C. Fischer and H. Wehrheim",
 year         = "2000",
 title        = "Behavioural subtyping relations for object-oriented formalisms",
 booktitle    = "AMAST 2000",
 series       = "LNCS",
 volume       = "1816",
 publisher    = "Springer",
 pages        = "469--483",
 doi          = "10.1007/3-540-45499-3\unhbox \voidb@x \kern 0.06em\vbox {\hrule width0.5em}33",
)
@inproceedings(Z-OO-Hall:1990,
 author       = "A. Hall",
 year         = "1990",
 title        = "Using {Z} as a Specification Calculus for Object-Oriented Systems",
 editor       = "A. Hoare and D. Bj\o {}rner and H. Langmaack",
 booktitle    = "VDM '90",
 series       = "LNCS",
 volume       = "428",
 publisher    = "Springer",
 pages        = "290--318",
 doi          = "10.1007/3-540-52513-0\unhbox \voidb@x \kern 0.06em\vbox {\hrule width0.5em}16",
)
@inproceedings(Z-OO-Hall:1994,
 author       = "A. Hall",
 year         = "1994",
 title        = "Specifying and Interpreting Class Hierarchies in {Z}",
 booktitle    = "{Z} User Workshop",
 series       = "Workshops in Computing",
 publisher    = "Springer",
 pages        = "120--138",
 doi          = "10.1007/978-1-4471-3452-7\unhbox \voidb@x \kern 0.06em\vbox {\hrule width0.5em}8",
)
@inproceedings(DataRef:HHS:1986,
 author       = "J. He and A. Hoare and J.W. Sanders",
 year         = "1986",
 title        = "Data Refinement Refined",
 booktitle    = "ESOP'86",
 series       = "LNCS",
 volume       = "213",
 publisher    = "Springer",
 pages        = "187--196",
 doi          = "10.1007/3-540-16442-1\unhbox \voidb@x \kern 0.06em\vbox {\hrule width0.5em}14",
)
@article(Hoare72:DR,
 author       = "A. Hoare",
 year         = "1972",
 title        = "Proof of Correctness of data representations",
 journal      = "Acta Informatica",
 volume       = "1",
 number       = "1",
 pages        = "271--281",
 doi          = "10.1007/BF00289507",
)
@book(Jackson:2006aa,
 author       = "D. Jackson",
 year         = "2006",
 title        = "Software Abstractions: logic, lanaguage, and analysis",
 publisher    = "MIT Press",
)
@article(Subtyping:LW:1994,
 author       = "B. Liskov and J. Wing",
 year         = "1994",
 title        = "A Behavioral Notion of Subtyping",
 journal      = "ACM Trans. Program. Lang. Syst.",
 volume       = "16",
 number       = "6",
 pages        = "1811--1841",
 doi          = "10.1145/197320.197383",
)
@inproceedings(Lupton:90,
 author       = "P.J. Lupton",
 year         = "1990",
 title        = "Promoting forward simulation",
 booktitle    = "Z User Workshop",
 publisher    = "Springer",
 pages        = "27--49",
)
@book(Meyer:97,
 author       = "B. Meyer",
 year         = "1997",
 title        = "Object-Oriented Software Construction",
 publisher    = "Prentice-Hall",
)
@book(OZSmith00,
 author       = "G.P. Smith",
 year         = "2000",
 title        = "The {Object-Z} Specification Language",
 publisher    = "Kluwer Academic Publishers",
 doi          = "10.1007/978-1-4615-5265-9",
)
@inproceedings(Stepney-etal:2003:ZB,
 author       = "S. Stepney and F. Polack and I. Toyn",
 year         = "2003",
 title        = "Patterns to Guide Practical Refactoring: examples targetting promotion in {Z}",
 booktitle    = "ZB 2003",
 series       = "LNCS",
 volume       = "2651",
 publisher    = "Springer",
 pages        = "20--39",
 doi          = "10.1007/3-540-44880-2\unhbox \voidb@x \kern 0.06em\vbox {\hrule width0.5em}3",
)
@inproceedings(Beh-Inh:W:2000,
 author       = "H. Wehrheim",
 year         = "2000",
 title        = "Behavioral Subtyping and property preservation",
 editor       = "S.F. Smith and C.L. Talcott",
 booktitle    = "FMOODS 2000",
 publisher    = "Kluwer",
 pages        = "213--231",
 doi          = "10.1007/978-0-387-35520-7\unhbox \voidb@x \kern 0.06em\vbox {\hrule width0.5em}11",
)
@book(UsingZ,
 author       = "J. Woodcock and J. Davies",
 year         = "1996",
 title        = "Using {Z}: Specification, Refinement, and Proof",
 publisher    = "Prentice-Hall",
)