@inproceedings(Bauer_01,
 author       = "Gertrud Bauer and Markus Wenzel",
 year         = "2001",
 title        = "Calculational Reasoning Revisited -- An Isabelle/Isar experience",
 booktitle    = "14th TPHOLs",
 publisher    = "Springer-Verlag",
 pages        = "75--90",
 doi          = "10.1007/3-540-44755-5\_7",
)
@article(Celiku_04,
 author       = "Orieta Celiku and Annabelle McIver",
 year         = "2004",
 title        = "Cost-based analysis of probabilistic programs mechanised in {HOL}",
 journal      = "Nordic J. of Computing",
 volume       = "11",
 number       = "2",
 pages        = "102--128",
 url          = "http://www.cse.unsw.edu.au/~carrollm/probs/Papers/ Celiku-04.pdf",
)
@inproceedings(Cock_11,
 author       = "David Cock",
 year         = "2011",
 title        = "Exploitation as an inference problem",
 booktitle    = "4th AISEC",
 address      = "Chicago, IL, USA",
 pages        = "105--106",
 doi          = "10.1145/2046684.2046702",
)
@inproceedings(Cock_KS_08,
 author       = "David Cock and Gerwin Klein and Thomas Sewell",
 year         = "2008",
 title        = "Secure Microkernels, State Monads and Scalable Refinement",
 editor       = "Otmane Ait Mohamed and C\'{e}sar Mu{\~{n}}oz and Sofi\`{e}ne Tahar",
 booktitle    = "21st TPHOLs",
 series       = "LNCS",
 volume       = "5170",
 publisher    = "Springer-Verlag",
 address      = "Montreal, Canada",
 pages        = "167--182",
 doi          = "10.1007/978-3-540-71067-7\_16",
)
@article(Dijkstra_75,
 author       = "Edsger W. Dijkstra",
 year         = "1975",
 title        = "Guarded commands, nondeterminacy and formal derivation of programs",
 journal      = "CACM",
 volume       = "18",
 number       = "8",
 pages        = "453--457",
 doi          = "10.1145/360933.360975",
)
@inproceedings(Goguen_Meseguer_82,
 author       = "Joseph Goguen and Jos{\'e} Meseguer",
 year         = "1982",
 title        = "Security Policies and Security Models",
 booktitle    = "IEEE Symp. Security \& Privacy",
 publisher    = "Comp. Soc.",
 address      = "Oakland, California, USA",
 pages        = "11--20",
)
@article(Harrison_05,
 author       = "William L. Harrison and Richard B. Kieburtz",
 year         = "2005",
 title        = "The logic of demand in Haskell",
 journal      = "J. Functional Progr.",
 volume       = "15",
 number       = "6",
 pages        = "837--891",
 doi          = "10.1017/S0956796805005666",
)
@article(Hurd_05,
 author       = "Joe Hurd and Annabelle McIver and Carroll Morgan",
 year         = "2005",
 title        = "Probabilistic guarded commands mechanized in HOL",
 journal      = "Theoretical Computer Science",
 volume       = "346",
 number       = "1",
 pages        = "96 -- 112",
 doi          = "10.1016/j.tcs.2005.08.005",
 url          = "http://www.sciencedirect.com/science/article/pii/ S0304397505004767",
)
@inproceedings(Klein_EHACDEEKNSTW_09,
 author       = "Gerwin Klein and Kevin Elphinstone and Gernot Heiser and June Andronick and David Cock and Philip Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish and Thomas Sewell and Harvey Tuch and Simon Winwood",
 year         = "2009",
 title        = "{seL4}: Formal Verification of an {OS} Kernel",
 booktitle    = "22nd SOSP",
 publisher    = "ACM",
 address      = "Big Sky, MT, USA",
 pages        = "207--220",
 doi          = "10.1145/1629575.1629596",
)
@article(McIver_01,
 author       = "Annabelle McIver and Carroll Morgan",
 year         = "2001",
 title        = "Partial correctness for probabilistic demonic programs",
 journal      = "Theoretical Comp. Sci.",
 volume       = "266",
 number       = "1\IeC {\textendash }2",
 pages        = "513 -- 541",
 doi          = "10.1016/S0304-3975(00)00208-5",
 url          = "http://www.sciencedirect.com/science/article/pii/ S0304397500002085",
)
@book(McIver_M_04,
 author       = "Annabelle McIver and Carroll Morgan",
 year         = "2004",
 title        = "Abstraction, Refinement and Proof for Probabilistic Systems",
 publisher    = "Springer",
)
@article(Mossakowski_10,
 author       = "Till Mossakowski and Lutz Schr\"oder and Sergey Goncharov",
 year         = "2010",
 title        = "A generic complete dynamic logic for reasoning about purity and effects",
 journal      = "Formal Aspects Comput.",
 volume       = "22",
 number       = "3-4",
 pages        = "363--384",
 doi          = "10.1007/s00165-010-0153-4",
)
@inproceedings(Nipkow_02,
 author       = "Tobias Nipkow",
 year         = "2002",
 title        = "Hoare Logics in {Isabelle/HOL}",
 editor       = "H. Schwichtenberg and R. Steinbr\"uggen",
 booktitle    = "Proof and System-Reliability",
 publisher    = "Kluwer",
 pages        = "341--367",
)
@book(Nipkow_PW:Isabelle,
 author       = "Tobias Nipkow and Lawrence Paulson and Markus Wenzel",
 year         = "2002",
 title        = "{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic",
 series       = "LNCS",
 volume       = "2283",
 publisher    = "Springer-Verlag",
)
@article(Selvin_75,
 author       = "Steve Selvin",
 year         = "1975",
 title        = "A problem in probability (letter to the editor)",
 journal      = "American Statistician",
 volume       = "29",
 number       = "1",
 pages        = "67",
)