@book(Abr11,
 author       = "J. R. Abrial",
 year         = "2010",
 title        = "{Modeling in Event-B}",
 publisher    = "Cambridge University Press",
 address      = "Cambridge, CB2 8BS, UK",
 doi          = "10.1017/CBO9781139195881",
)
@inproceedings(Back90,
 author       = "R. J. R. Back",
 year         = "1990",
 title        = "{Refinement Calculus, Part II: Parallel and Reactive Programs}",
 booktitle    = "Stepwise Refinement of Distributed Systems Models, Formalisms, Correctness",
 series       = "LNCS",
 volume       = "430",
 publisher    = "Springer",
 pages        = "67--93",
 doi          = "10.1007/3-540-52559-9\unhbox \voidb@x \kern 0.06em\vbox {\hrule width0.5em}61",
)
@inproceedings(BK83,
 author       = "R. J. R. Back and R. Kurki-Suonio",
 year         = "1983",
 title        = "{Decentralization of Process Nets with Centralized Control}",
 booktitle    = "Proceedings of PODC '83",
 publisher    = "ACM",
 pages        = "131--142",
 doi          = "10.1145/800221.806716",
)
@article(BW03,
 author       = "R. J. R. Back and J. von Wright",
 year         = "2003",
 title        = "{Compositional Action System Refinement}",
 journal      = "Formal Aspects of Computing",
 volume       = "15",
 pages        = "103--117",
 doi          = "10.1007/s00165-003-0005-6",
)
@article(Bur99,
 author       = "A. Burns",
 year         = "1999",
 title        = "{The Ravenscar Profile}",
 journal      = "ACM SIGAda Ada Letters",
 volume       = "XIX",
 pages        = "49--52",
 doi          = "10.1145/340396.340450",
)
@inproceedings(But09,
 author       = "M. Butler",
 year         = "2009",
 title        = "{Decomposition Structures for Event-B}",
 booktitle    = "Proceedings of IFM 2009",
 series       = "LNCS",
 volume       = "5423",
 publisher    = "Springer",
 address      = "D{\"u}sseldorf, Germany",
 pages        = "20--38",
 doi          = "10.1007/978-3-642-00255-7\unhbox \voidb@x \kern 0.06em\vbox {\hrule width0.5em}2",
)
@inproceedings(CMR06,
 author       = "D. Cansell and D. M{\'e}ry and J. Rehm",
 year         = "2006",
 title        = "{Time Constraint Patterns for Event B Development}",
 booktitle    = "Proceedings of B 2007",
 series       = "LNCS",
 volume       = "4355",
 publisher    = "Springer",
 address      = "Besan\c {c}on, France",
 pages        = "140--154",
 doi          = "10.1007/11955757\unhbox \voidb@x \kern 0.06em\vbox {\hrule width0.5em}13",
)
@phdthesis(ZRC,
 author       = "A. Cavalcanti",
 year         = "1997",
 title        = "{A Refinement Calculus for Z}",
 school       = "University of Oxford, UK",
 address      = "Oxford, OX1 3QD, UK",
 url          = "http://www.cs.ox.ac.uk/files/3451/PRG123.pdf",
)
@article(CSW03,
 author       = "A. Cavalcanti and A. Sampaio and J. Woodcock",
 year         = "2003",
 title        = "{A Refinement Strategy for {{\sf \slshape Circus}}}",
 journal      = "Formal Aspects of Computing",
 volume       = "15",
 pages        = "146--181",
 doi          = "10.1007/s00165-003-0006-5",
)
@article(CSW05,
 author       = "A. Cavalcanti and A. Sampaio and J. Woodcock",
 year         = "2005",
 title        = "{Unifying classes and processes}",
 journal      = "Software and Systems Modeling",
 volume       = "4",
 number       = "3",
 pages        = "277--296",
 doi          = "10.1007/s10270-005-0085-2",
)
@inproceedings(CWW11,
 author       = "A. Cavalcanti and A. Wellings and J. Woodcock",
 year         = "2011",
 title        = "{The Safety-Critical Java Memory Model: A Formal Account}",
 booktitle    = "Proceedings of FM 2011",
 series       = "LNCS",
 volume       = "6664",
 publisher    = "Springer",
 address      = "Limerick, Ireland",
 pages        = "246--261",
 doi          = "10.1007/978-3-642-21437-0\unhbox \voidb@x \kern 0.06em\vbox {\hrule width0.5em}20",
)
@article(CZWWW12,
 author       = "A. Cavalcanti and F. Zeyda and A. Wellings and J. Woodcock and K. Wei",
 year         = "2012",
 title        = "{Safety-Critical java programs from {{\sf \slshape Circus}} models}",
 journal      = "Real-time Systems",
 doi          = "10.1007/s11241-013-9182-4",
 note         = "Under publication.",
)
@inproceedings(DHS12,
 author       = "A. Dalsgaard and R. Hansen and M. Schoeberl",
 year         = "2012",
 title        = "{Private Memory Allocation Analysis for Safety-Critical Java}",
 booktitle    = "Proceedings of JTRES 2012",
 publisher    = "ACM",
 pages        = "9--17",
 doi          = "10.1145/2388936.2388939",
)
@article(Gro02,
 author       = "L. Groves",
 year         = "2002",
 title        = "{Refinement and the Z Schema Calculus}",
 journal      = "Electronic Notes in Theoretical Computer Science",
 volume       = "70",
 pages        = "70--93",
 doi          = "10.1016/S1571-0661(05)80486-4",
)
@inproceedings(HL11,
 author       = "G. Haddad and G. Leavens",
 year         = "2011",
 title        = "{Specifying Subtypes in SCJ Programs}",
 booktitle    = "Proceedings of JTRES 2011",
 publisher    = "ACM",
 pages        = "40--46",
 doi          = "10.1145/2043910.2043917",
)
@inproceedings(HHLNSV09,
 author       = "T. Henties and J. Hunt and D. Locke and K. Nilsen and M. Schoeberl and J. Vitek",
 year         = "2009",
 title        = "{Java for Safety-Critical Applications}",
 booktitle    = "Proceedings of SafeCert 2009",
 address      = "York, UK",
 pages        = "1--11",
 url          = "http://www.vmars.tuwien.ac.at/php/pserver/extern/download.php?fileid=1641",
)
@book(HH98,
 author       = "C. A. R. Hoare and H. Jifeng",
 year         = "1998",
 title        = "{Unifying Theories of Programming}",
 series       = "Prentice Hall Series in Computer Science",
 publisher    = "Prentice Hall",
 address      = "Upper Saddle River, NJ, USA",
)
@inproceedings(KHPPTV09,
 author       = "T. Kalibera and J. Hagelberg and F. Pizlo and A. Plsek and B. Titzer and J. Vitek",
 year         = "2009",
 title        = "{{\textsf {CD}$_{x}$}: A Family of Real-time Java Benchmarks}",
 booktitle    = "Proceedings of JTRES 2009",
 publisher    = "ACM",
 pages        = "41--50",
 doi          = "10.1145/1620405.1620412",
)
@book(Mor90,
 author       = "C. C. Morgan",
 year         = "1990",
 title        = "{Programming from Specifications}",
 series       = "Prentice Hall International Series in Computer Science",
 publisher    = "Prentice Hall",
 address      = "Upper Saddle River, NJ, USA",
)
@phdthesis(Oli05,
 author       = "M. Oliveira",
 year         = "2005",
 title        = "{Formal Derivation of State-Rich Reactive Programs using {{\sf \slshape Circus}}}",
 school       = "University of York",
 address      = "York, YO10 5GH, UK",
 url          = "http://www.cs.york.ac.uk/circus/publications/papers/06-oliveira.pdf",
)
@article(OCW09,
 author       = "M. Oliveira and A. Cavalcanti and J. Woodcock",
 year         = "2009",
 title        = "{A UTP semantics for {{\sf \slshape Circus}}}",
 journal      = "Formal Aspects of Computing",
 volume       = "21",
 pages        = "3--32",
 doi          = "10.1007/s00165-007-0052-5",
)
@book(Ros97,
 author       = "A. W. Roscoe",
 year         = "1997",
 title        = "{The Theory and Practice of Concurrency}",
 series       = "Prentice Hall Series in Computer Science",
 publisher    = "Prentice Hall",
 address      = "Upper Saddle River, NJ, USA",
)
@article(SCJS09,
 author       = "A. Sherif and A. Cavalcanti and H. Jifeng and A. Sampaio",
 year         = "2009",
 title        = "{A process algebraic framework for specification and validation of real-time systems}",
 journal      = "Formal Aspects of Computing",
 volume       = "22",
 pages        = "153--191",
 doi          = "10.1007/s00165-009-0119-6",
)
@inproceedings(STR06,
 author       = "H. S{\o }ndergaard and B Thomsen and A. P. Ravn",
 year         = "2006",
 title        = "{A Ravenscar-Java Profile Implementation}",
 booktitle    = "Proceedings of JTRES 2006",
 publisher    = "ACM",
 address      = "Paris, France",
 pages        = "38--47",
 doi          = "10.1145/1167999.1168008",
)
@inproceedings(TPV10,
 author       = "D. Tang and A. Plsek and J. Vitek",
 year         = "2010",
 title        = "{Static Checking of Safety Critical Java Annotations}",
 booktitle    = "Proceedings of JTRES 2010",
 publisher    = "ACM",
 pages        = "148--154",
 doi          = "10.1145/1850771.1850792",
)
@techreport(JSR302,
 author       = "{The Open Group}",
 year         = "2011",
 title        = "{Safety Critical Java Technology Specification}",
 type         = "Technical Report",
 number       = "JSR-302",
 institution  = "Java Community Process",
 url          = "http://jcp.org/en/jsr/detail?id=302",
)
@book(Wel04,
 author       = "A. Wellings",
 year         = "2004",
 title        = "{Concurrent and Real-Time Programming in Java}",
 publisher    = "Wiley",
 address      = "West Sussex, PO19 8SQ, UK",
)
@book(WD96,
 author       = "J. Woodcock and J. Davies",
 year         = "1996",
 title        = "{Using Z:~ Specification, Refinement and Proof}",
 series       = "Prentice Hall International Series in Computer Science",
 publisher    = "Prentice Hall",
 address      = "Upper Saddle River, NJ, USA",
)
@inproceedings(ZCW11,
 author       = "F. Zeyda and A. Cavalcanti and A. Wellings",
 year         = "2011",
 title        = "{The Safety-Critical Java Mission Model: A Formal Account}",
 booktitle    = "Proceedings of ICFEM 2011",
 series       = "LNCS",
 volume       = "6991",
 publisher    = "Springer",
 address      = "Durham, UK",
 pages        = "49--65",
 doi          = "10.1007/978-3-642-24559-6\unhbox \voidb@x \kern 0.06em\vbox {\hrule width0.5em}6",
)
@techreport(ZCWWW12,
 author       = "F. Zeyda and A. Cavalcanti and A. Wellings and J. Woodcock and K. Wei",
 year         = "2012",
 title        = "{Refinement of the Parallel {\textsf {CD}$_{x}$}}",
 type         = "Technical Report",
 institution  = "University of York",
 address      = "York, UK",
 url          = "http://www.cs.york.ac.uk/circus/publications/techreports/",
)
@article(ZOC12,
 author       = "F. Zeyda and M. Oliveira and A. Cavalcanti",
 year         = "2012",
 title        = "{Mechanised support for sound refinement tactics}",
 journal      = "Formal Aspects of Computing",
 volume       = "24",
 number       = "1",
 pages        = "127--160",
 doi          = "10.1007/s00165-011-0218-z",
)