@book(BBook,
 author       = "J. R. Abrial",
 year         = "1996",
 title        = "The B-Book: Assigning programs to meaning.",
 publisher    = "Cambridge University Press",
)
@book(Event-B,
 author       = "J. R. Abrial",
 year         = "2009",
 title        = "Modeling in Event-B: system and software engineering. To appear",
 publisher    = "Cambridge University Press",
 url          = "http://www.event-b.org",
)
@inproceedings(Airbag,
 author       = "H. Aljazzar and M. Fischer and L. Grunske and M. Kuntz and F. Leitner and S. Leue",
 year         = "2009",
 title        = "Safety analysis of an airbag system using probabilistic FMEA and probabilistic counterexamples",
 publisher    = "In proceedings of QEST'09",
 pages        = "299--308",
 doi          = "10.1109/QEST.2009.8",
)
@inproceedings(HL09,
 author       = "H. Aljazzar and S. Leue",
 year         = "2009",
 title        = "Generation of counterexamples for model checking of Markov Decision Processes",
 publisher    = "In proceedings of QEST'09",
 pages        = "197--206",
 doi          = "10.1109/QEST.2009.10",
)
@inproceedings(ADR09,
 author       = "M. E. Andr$\mathaccent "7013\relax {e}$s and P. D' Argenio and P. v Rossum",
 year         = "2009",
 title        = "Significant diagnostic counterexamples in probabilistic model checking",
 publisher    = "In proceedings of HVC'08. Lecture Notes in Computer Science 5394",
 pages        = "129--148",
 doi          = "10.1007/978-3-642-01702-5_15",
)
@techreport(Butler09,
 author       = "M. Butler",
 year         = "2009",
 title        = "Using Event-B refinement to verify a control strategy",
 type         = "Technical Report",
 institution  = "University of Southampton",
 address      = "United Kingdom",
)
@inproceedings(CMR,
 author       = "D. Cansell and D. M$\mathaccent "7012\relax {e}$ry and J. Rehm",
 year         = "2006",
 title        = "Time constraint patterns for Event-B development",
 publisher    = "In proceedings of B'07. Lecture Notes in Computer Science 4355. Springer",
 pages        = "140--154",
 doi          = "10.1007/11955757_13",
)
@manual(HAZOP,
 organization = "Chemical Industries Association Limited",
 address      = "London",
 year         = "1987",
 title        = "CIA.: A guide to hazard and operability studies.",
)
@inproceedings(DEPLOY,
 title        = "Deploy",
 url          = "http://www.deploy-project.eu/",
)
@inproceedings(pFMEA,
 author       = "L. Grunske and R. Colvin and K. Winter",
 year         = "2007",
 title        = "Probabilistic model checking support for FMEA",
 publisher    = "In proceedings of QEST'07",
 doi          = "10.1109/QEST.2007.18",
)
@inproceedings(GO10,
 author       = "M. G{u}demann and F. Ortmeier",
 year         = "2010",
 title        = "Probabilistic model-based safety analysis",
 publisher    = "In proceedings of QAPL'10. EPTCS 28",
 pages        = "114--128",
 doi          = "10.4204/EPTCS.28.8",
)
@article(TJB09,
 author       = "T. Han and J.-P Katoen and B. Damman",
 year         = "2009",
 title        = "Counterexamples generation in probabilistic model checking",
 journal      = "IEEE Transaction on software engineering",
 volume       = "32",
 number       = "2",
 pages        = "241--257",
 doi          = "10.1007/978-3-540-71209-1_8",
)
@article(pCTL,
 author       = "H. Hansson and B. Jonsson",
 year         = "1994",
 title        = "A logic for reasoning about time and reliability",
 journal      = "Formal Aspects of Computing",
 volume       = "6",
 number       = "5",
 pages        = "512--535",
 doi          = "10.1007/BF01211866",
)
@inproceedings(PRISM,
 author       = "A. Hinton and M. Kwiatkowska and G. Norman and D. Parker",
 year         = "2006",
 title        = "PRISM: A tool for automatic verification of probabilistic systems",
 publisher    = "In proceedings of TACAS'06. Lecture Notes in Computer Science 3920. Springer",
 pages        = "441--444",
 doi          = "10.1007/11691372_29",
)
@phdthesis(Hoang05,
 author       = "T. S. Hoang",
 year         = "2005",
 title        = "Developing a probabilistic B-Method and a supporting toolkit.",
 school       = "University of New South Wales",
 address      = "Australia",
)
@article(Hoare,
 author       = "C. A. R. Hoare",
 year         = "1969",
 title        = "An axiomatic basis for computer programming",
 journal      = "Communications of the ACM",
 volume       = "12",
 number       = "10",
 pages        = "576--580",
 doi          = "10.1145/357980.358001",
)
@phdthesis(Hurd,
 author       = "J. Hurd",
 year         = "2002",
 title        = "Formal verification of probabilistic algorithms.",
 school       = "University of Cambridge",
 address      = "United Kingdom",
)
@manual(FMEA,
 organization = "Internatinal Electrotechnical Commission",
 address      = "Geneva",
 year         = "1985",
 title        = "IEC International Standard 812: ``Analysis techniques for system reliability: procedures for failure mode and effect analysis",
)
@manual(FTA,
 organization = "Internatinal Electrotechnical Commission",
 address      = "Geneva",
 year         = "1990",
 title        = "International Standard IEC 1025: Fault Tree Analysis (FTA).",
)
@inproceedings(Karger,
 author       = "D.R. Karger",
 year         = "1993",
 title        = "Global min-cuts in RNC, and other ramifications of a simple min-out algorithm",
 publisher    = "In proceedings of fourth annual ACM-SIAM symposium on discrete algorithms. pp 21-30",
 address      = "Austin, Texas, United States",
)
@article(KNP04,
 author       = "M. Kwiatkowska and G. Norman and D. Parker",
 year         = "2007",
 title        = "Controller dependability analysis by probabilistic model checking",
 journal      = "Control Engineering Practice",
 volume       = "15",
 number       = "11",
 pages        = "1427--1434",
 doi          = "10.1016/j.conengprac.2006.07.003",
)
@book(MM04,
 author       = "A.K. McIver and C.C. Morgan",
 year         = "2004",
 title        = "Abstraction, refinement and proof for probabilistic systems",
 publisher    = "Monographs in Computer Science. Springer Verlag",
)
@inproceedings(UNdukwu,
 author       = "U. Ndukwu",
 year         = "2009",
 title        = "Quantitative safety: linking proof-based verification with model checking for probabilistic systems",
 publisher    = "In proceedings of QFM'09. EPTCS 13",
 pages        = "27--39",
 doi          = "10.4204/EPTCS.13.3",
)
@inproceedings(Ndukwu11,
 author       = "U. Ndukwu",
 year         = "2010",
 title        = "Generating counterexamples for quantitative safety specifications in probabilistic B",
 publisher    = "Accepted for inclusion in the journal of logic and algebraic programming",
)
@inproceedings(YAGA,
 author       = "U. Ndukwu and A.K. McIver",
 year         = "2010",
 title        = "YAGA: Automated analysis of quantitative safety specifications in probabilistic B",
 publisher    = "In proceedings of ATVA'10. Lecture Notes in Computer Science 6252. Springer",
 pages        = "378--386",
 doi          = "10.1007/978-3-642-15643-4_31",
)
@inproceedings(DCCA,
 author       = "F. Ortmeier and W. Reif and G. Schellhorn",
 year         = "2006",
 title        = "Deductive cause-consequence analysis (DCCA)",
 publisher    = "In proceedings of IFAC World Congress, Elsevier",
)
@book(MDP,
 author       = "M.L. Puterman",
 year         = "1994",
 title        = "Markov Decision Processes.",
 publisher    = "Wiley",
)