@inproceedings(andova2003rewardsmodel,
 author       = "S.~{Andova} and H.~{Hermanns} and J.-P. {Katoen}",
 year         = "2003",
 title        = "Discrete-time rewards model-checked",
 editor       = "K.~G. {Larsen} and P.~{Niebert}",
 booktitle    = "FORMATS",
 series       = "LNCS",
 volume       = "2791",
 pages        = "88--104",
 doi          = "10.1007/978-3-540-40903-8\_8",
)
@article(audebaud2009randomizedalgos,
 author       = "P.~Audebaud and C.~Paulin-Mohring",
 year         = "2009",
 title        = "Proofs of randomized algorithms in {Coq}",
 journal      = "Science of Computer Programming",
 volume       = "74",
 number       = "8",
 pages        = "568--589",
 doi          = "10.1016/j.scico.2007.09.002",
)
@phdthesis(baier1998habil,
 author       = "C.~Baier",
 year         = "1998",
 title        = "On the Algorithmic Verification of Probabilistic Systems",
 type         = "Habilitation",
 school       = "U. Mannheim",
)
@book(baier2008modelchecking,
 author       = "C.~Baier and J.-P. Katoen",
 year         = "2008",
 title        = "Principles of Model Checking",
 publisher    = "The MIT Press",
 address      = "Cambridge, Massachusetts",
)
@inproceedings(bohnenkamp2003zeroconfcost,
 author       = "H.~Bohnenkamp and P.~van~der Stok and H.~Hermanns and F.~Vaandrager",
 year         = "2003",
 title        = "Cost-Optimisation of the IPv4 Zeroconf Protocol",
 booktitle    = "DSN'03",
 publisher    = "IEEE CS Press",
 pages        = "531--540",
 doi          = "10.1109/DSN.2003.1209963",
)
@misc(cheshire2005zeroconf,
 author       = "S.~Cheshire and B.~Aboba and E.~Guttman",
 year         = "2005",
 title        = "Dynamic Configuration of {IPv4} Link-Local Addresses",
 howpublished = "RFC 3927 (Proposed Standard)",
 url          = "http://www.ietf.org/rfc/rfc3927.txt",
)
@phdthesis(coble09thesis,
 author       = "A.~R. Coble",
 year         = "2009",
 title        = "Anonymity, Information, and Machine-Assisted Proof",
 school       = "U. of Cambridge",
)
@article(hahn2011parametricmc,
 author       = "E.~M. Hahn and H.~Hermanns and L.~Zhang",
 year         = "2011",
 title        = "Probabilistic reachability for parametric Markov models",
 journal      = "Int. J. on Software Tools for Technology Transfer (STTT)",
 volume       = "13",
 number       = "1",
 pages        = "3--19",
 doi          = "10.1007/s10009-010-0146-x",
)
@inproceedings(hasan2009expectation,
 author       = "O.~Hasan and N.~Abbasi and B.~Akbarpour and S.~Tahar and R.~Akbarpour",
 year         = "2009",
 title        = "Formal Reasoning about Expectation Properties for Continuous Random Variables",
 editor       = "A.~Cavalcanti and D.~Dams",
 booktitle    = "Formal Methods (FM 2009)",
 series       = "LNCS",
 volume       = "5850",
 pages        = "435--450",
 doi          = "10.1007/978-3-642-05089-3\_28",
)
@inproceedings(hermanns2008pcegar,
 author       = "H.~Hermanns and B.~Wachter and L.~Zhang",
 year         = "2008",
 title        = "Probabilistic {CEGAR}",
 editor       = "A.~Gupta and S.~Malik",
 booktitle    = "Computer Aided Verification (CAV 2008)",
 series       = "LNCS",
 volume       = "5123",
 pages        = "162--175",
 doi          = "10.1007/978-3-540-70545-1\_16",
)
@inproceedings(hoelzl2011measure,
 author       = "J.~H{\"o}lzl and A.~Heller",
 year         = "2011",
 title        = "Three Chapters of Measure Theory in {Isabelle/HOL}",
 editor       = "M.~C. J.~D. van Eekelen and H.~Geuvers and J.~Schmaltz and F.~Wiedijk",
 booktitle    = "ITP 2011",
 series       = "LNCS",
 volume       = "6898",
 pages        = "135--151",
 doi          = "10.1007/978-3-642-22863-6\_12",
)
@inproceedings(hoelzl2012verifyingpctl,
 author       = "J.~H{\"o}lzl and T.~Nipkow",
 year         = "2012",
 title        = "Verifying {pCTL} Model Checking",
 editor       = "C.~Flanagan and B.~K\IeC {\"o}nig",
 booktitle    = "TACAS 2012",
 series       = "LNCS",
 volume       = "7214",
 pages        = "347--361",
 doi          = "10.1007/978-3-642-28756-5\_24",
)
@phdthesis(hurd02thesis,
 author       = "J.~Hurd",
 year         = "2002",
 title        = "Formal Verification of Probabilistic Algorithms",
 school       = "U. of Cambridge",
)
@article(hurd05pgcl,
 author       = "J.~Hurd and A.~McIver and C.~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",
)
@article(hoelzl2012afp-markov,
 author       = "J.~H\IeC {\"o}lzl and T.~Nipkow",
 year         = "2012",
 title        = "Markov Models",
 journal      = "The Archive of Formal Proofs",
 note         = "\url {http://afp.sf.net/entries/Markov\_Models.shtml}, Formal proof development",
)
@inproceedings(katoen2010invariant,
 author       = "J.-P. Katoen and A.~McIver and L.~Meinicke and C.~C. Morgan",
 year         = "2010",
 title        = "Linear-Invariant Generation for Probabilistic Programs: - Automated Support for Proof-Based Methods",
 editor       = "R.~Cousot and M.~Martel",
 booktitle    = "Static Analysis (SAS 2010)",
 series       = "LNCS",
 volume       = "6337",
 pages        = "390--406",
 doi          = "10.1007/978-3-642-15769-1\_24",
)
@inproceedings(kwiatkowska2011prism4,
 author       = "M.~Kwiatkowska and G.~Norman and D.~Parker",
 year         = "2011",
 title        = "{PRISM} 4.0: Verification of Probabilistic Real-time Systems",
 series       = "LNCS",
 volume       = "6806",
 doi          = "10.1007/978-3-642-22110-1\_47",
)
@article(KNPS06,
 author       = "M.~Kwiatkowska and G.~Norman and D.~Parker and J.~Sproston",
 year         = "2006",
 title        = "Performance Analysis of Probabilistic Timed Automata using Digital Clocks",
 journal      = "FM in System Design",
 volume       = "29",
 pages        = "33--78",
 doi          = "10.1007/s10703-006-0005-2",
)
@inproceedings(liu2011markovchains,
 author       = "L.~Liu and O.~Hasan and S.~Tahar",
 year         = "2011",
 title        = "Formalization of Finite-State Discrete-Time Markov Chains in {HOL}",
 editor       = "T.~Bultan and P.-A. Hsiung",
 booktitle    = "ATVA 2011",
 series       = "LNCS",
 volume       = "6996",
 pages        = "90--104",
 doi          = "10.1007/978-3-642-24372-1\_8",
)
@inproceedings(malacaria2007securitythreats,
 author       = "P.~Malacaria",
 year         = "2007",
 title        = "Assessing Security Threats of Looping Constructs",
 booktitle    = "{ACM SIGPLAN} Symposium on Principles of Programming Languages {(POPL'07)}",
 pages        = "225--235",
 doi          = "10.1145/1190215.1190251",
)
@book(nipkow2002isabelle,
 author       = "T.~Nipkow and L.~C. Paulson and M.~Wenzel",
 year         = "2002",
 title        = "Isabelle/{HOL}: A Proof Assistant for Higher-Order Logic",
 series       = "LNCS",
 volume       = "2283",
 publisher    = "Springer",
 doi          = "10.1007/3-540-45949-9",
)
@article(reiter1998crowds,
 author       = "M.~Reiter and A.~Rubin",
 year         = "1998",
 title        = "Crowds: Anonymity for web transactions",
 journal      = "ACM Transactions on Information and System Security (TISSEC)",
 volume       = "1",
 number       = "1",
 pages        = "66--92",
 doi          = "10.1145/290163.290168",
)
@article(Shmatikov04,
 author       = "V.~Shmatikov",
 year         = "2004",
 title        = "Probabilistic analysis of an anonymity system",
 journal      = "J. of Comp. Sec.",
 volume       = "12",
 pages        = "355--377",
)