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