@techreport(BackKarttunen83PredicateTransformerMultipleExits,
 author       = "R.-J. R. Back and M. Karttunen",
 year         = "1983",
 title        = "A predicate transformer semantics for statements with multiple exits",
 type         = "Unpublished manuscript",
 institution  = "University of Helsinki",
)
@book(BackVonWright98RefinementCalculus,
 author       = "Ralph-Johan Back and Joakim von Wright",
 year         = "1998",
 title        = "Refinement Calculus: A Systematic Introduction",
 publisher    = "Springer-Verlag",
 doi          = "10.1007/978-1-4612-1674-2",
)
@article(Back81CorrectRefinement,
 author       = "R.J.R. Back",
 year         = "1981",
 title        = "On correct refinement of programs",
 journal      = "Journal of Computer and System Sciences",
 volume       = "23",
 number       = "1",
 pages        = "49 -- 68",
 doi          = "10.1016/0022-0000(81)90005-2",
)
@article(BanachaPoppletonJeskeaStepney07Retrenchment,
 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",
)
@inproceedings(BoitenDerrick98IORefinement,
 author       = "E. Boiten and J. Derrick",
 year         = "1998",
 title        = "IO-Refinement in Z",
 booktitle    = "Proc. Third BCS-FACS Northern Formal Methods Workshop, Ilkley, UK",
 publisher    = "http://www.ewic.org.uk/ewic/workshop/view.cfm/NFM-98.",
)
@article(Cristian84CorrectRobustPrograms,
 author       = "Flaviu Cristian",
 year         = "1984",
 title        = "Correct and Robust Programs",
 journal      = "IEEE Transactions on Software Engineering",
 volume       = "10",
 number       = "2",
 pages        = "163--174",
 doi          = "10.1109/TSE.1984.5010218",
)
@book(DerrickBoiten01RefinementZObjectZ,
 author       = "J. Derrick and E. Boiten",
 year         = "2001",
 title        = "Refinement in Z and Object-Z, Foundations and Advanced Applications",
 series       = "Formal Approaches to Computing and Information Technology",
 publisher    = "Springer",
 doi          = "10.1002/stvr.237",
)
@article(Dijkstra75GuardedCommands,
 author       = "Edsger W. Dijkstra",
 year         = "1975",
 title        = "Guarded commands, nondeterminacy and formal derivation of programs",
 journal      = "Commun. ACM",
 volume       = "18",
 number       = "8",
 pages        = "453--457",
 doi          = "10.1145/360933.360975",
)
@article(GardinerMorgan93RuleDataRefinement,
 author       = "P. H. B. Gardiner and Carroll Morgan",
 year         = "1993",
 title        = "A single complete rule for data refinement",
 journal      = "Formal Aspects of Computing",
 volume       = "5",
 number       = "4",
 pages        = "367--382",
 doi          = "10.1007/BF01212407",
)
@article(GardinerMorgan91DataRefinementPredicateTransformer,
 author       = "Paul Gardiner and Carroll Morgan",
 year         = "1991",
 title        = "Data refinement of predicate transformers",
 journal      = "Theoretical Computer Science",
 volume       = "87",
 number       = "1",
 pages        = "143 -- 162",
 doi          = "10.1016/0304-3975(91)90029-2",
)
@(Intel13Assembly,
 author       = "Intel",
 year         = "2013",
 title        = "Intel® 64 and IA-32 Architectures Software Developer’s Manual, Volume 2 (2A, 2B \& 2C): Instruction Set Reference, A-Z",
 url          = "http://download.intel.com/products/processor/manual/325383.pdf",
)
@inproceedings(Jacobs01FormalisationJavaExceptions,
 author       = "Bart Jacobs",
 year         = "2001",
 title        = "A Formalisation of Java's Exception Mechanism",
 editor       = "D. Sands",
 booktitle    = "ESOP '01: Proceedings of the 10th European Symposium on Programming Languages and Systems",
 publisher    = "Springer-Verlag",
 address      = "London, UK",
 pages        = "284--301",
 doi          = "10.1007/3-540-45309-1\_19",
)
@article(JacobsGries85GeneralCorrectness,
 author       = "Dean Jacobs and David Gries",
 year         = "1985",
 title        = "General correctness: a unification of partial and total correctness",
 journal      = "Acta Inf.",
 volume       = "22",
 number       = "1",
 pages        = "67--83",
 doi          = "10.1007/BF00290146",
)
@incollection(JeffordsHeitmeyerArcherLeonard09CorrectFaultTolerantSystems,
 author       = "Ralph Jeffords and Constance Heitmeyer and Myla Archer and Elizabeth Leonard",
 year         = "2009",
 title        = "A Formal Method for Developing Provably Correct Fault-Tolerant Systems Using Partial Refinement and Composition",
 editor       = "Ana Cavalcanti and DennisR. Dams",
 booktitle    = "FM 2009: Formal Methods",
 series       = "Lecture Notes in Computer Science",
 volume       = "5850",
 publisher    = "Springer Berlin Heidelberg",
 pages        = "173--189",
 doi          = "10.1007/978-3-642-05089-3\_12",
)
@article(KingMorgan95ExitsInRefinementCalculus,
 author       = "Steve King and Carroll Morgan",
 year         = "1995",
 title        = "Exits in the Refinement Calculus",
 journal      = "Formal Aspects of Computing",
 volume       = "7",
 number       = "1",
 pages        = "54--76",
 doi          = "10.1007/BF01214623",
)
@inproceedings(LeinoSnepscheut94SemanticsExceptions,
 author       = "K. Rustan M. Leino and Jan L. A. van de Snepscheut",
 year         = "1994",
 title        = "Semantics of Exceptions",
 editor       = "Ernst-R{\"u}diger Olderog",
 booktitle    = "PROCOMET '94: Proceedings of the IFIP TC2/WG2.1/WG2.2/WG2.3 Working Conference on Programming Concepts, Methods and Calculi",
 series       = "IFIP Transactions A-56",
 publisher    = "North-Holland Publishing Co.",
 pages        = "447--466",
 url          = "http://authors.library.caltech.edu/26774/2/93-34.pdf",
)
@article(ManoharLeino95ConditionalComposition,
 author       = "Rajit Manohar and K. Rustan M. Leino",
 year         = "1995",
 title        = "Conditional Composition",
 journal      = "Formal Aspects of Computing",
 volume       = "7",
 number       = "6",
 pages        = "683--703",
 doi          = "10.1007/BF01211001",
)
@book(Meyer97OOSoftwareConstruction,
 author       = "Bertrand Meyer",
 year         = "1997",
 title        = "Object-Oriented Software Construction",
 edition      = "2nd",
 publisher    = "Prentice-Hall, Inc.",
)
@(MS13NotImplementedException,
 author       = "Microsoft",
 year         = "2013",
 title        = "NotImplementedException Class",
 url          = "http://msdn.microsoft.com/en-us/library/system.notimplementedexception.aspx",
)
@(MS13OverflowException,
 author       = "Microsoft",
 year         = "2013",
 title        = "OverflowException Class",
 url          = "http://msdn.microsoft.com/en-us/library/system.overflowexception.aspx",
)
@inproceedings(MikhajlovaSekerinski97ClassInterfaceRefinement,
 author       = "Anna Mikhajlova and Emil Sekerinski",
 year         = "1997",
 title        = "Class Refinement and Interface Refinement in Object-Oriented Programs",
 editor       = "John Fitzgerald and Cliff Jones and Peter Lucas",
 booktitle    = "FME '97: Industrial Applications and Strengthened Foundations of Formal Methods",
 series       = "Lecture Notes in Computer Science",
 volume       = "1313",
 publisher    = "Springer-Verlag",
 pages        = "82--101",
 doi          = "10.1007/3-540-63533-5\_5",
)
@inproceedings(Parnas78ExtensionContraction,
 author       = "David L. Parnas",
 year         = "1978",
 title        = "Designing software for ease of extension and contraction",
 booktitle    = "Proceedings of the 3rd international conference on Software engineering",
 series       = "ICSE '78",
 publisher    = "IEEE Press",
 address      = "Piscataway, NJ, USA",
 pages        = "264--277",
 doi          = "10.1109/TSE.1979.234169",
)
@inproceedings(SekerinskiZhang11PartialCorrectness,
 author       = "Emil Sekerinski and Tian Zhang",
 year         = "2011",
 title        = "A New Notion of Partial Correctness for Exception Handling",
 editor       = "Borzoo Bonakdarpour and Tom Maibaum",
 booktitle    = "Proceedings of the 2nd International Workshop on Logical Aspects of Fault-Tolerance",
 pages        = "116--132",
 url          = "https://ece.uwaterloo.ca/~bbonakda/LAFT11/papers/proc.pdf",
)
@incollection(StepneyCooperWoodcock98ZDataRefinement,
 author       = "Susan Stepney and David Cooper and Jim Woodcock",
 year         = "1998",
 title        = "More Powerful {Z} Data Refinement: Pushing the State of the Art in Industrial Refinement",
 editor       = "Jonathan P. Bowen and Andreas Fett and Michael G. Hinchey",
 booktitle    = "ZUM '98: The Z Formal Specification Notation",
 series       = "Lecture Notes in Computer Science",
 volume       = "1493",
 publisher    = "Springer Berlin Heidelberg",
 pages        = "284--307",
 doi          = "10.1007/978-3-540-49676-2\_20",
)
@inproceedings(Watson02RefiningExceptions,
 author       = "G. Watson",
 year         = "2002",
 title        = "Refining exceptions using {King} and {Morgan}'s exit construct",
 booktitle    = "Software Engineering Conference, 2002. Ninth Asia-Pacific",
 pages        = "43--51",
 doi          = "10.1109/APSEC.2002.1182974",
)
@article(vonWright94LatticeDataRefinement,
 author       = "J. von Wright",
 year         = "1994",
 title        = "The lattice of data refinement",
 journal      = "Acta Informatica",
 volume       = "31",
 number       = "2",
 pages        = "105--135",
 doi          = "10.1007/BF01192157",
)