1Christel Baier , Joost-Pieter Katoen, Principles of Model Checking (Representation and Mind Series), The MIT Press, 2008
 	
2Christel Baier , Boudewijn Haverkort , Holger Hermanns , Joost-Pieter Katoen, Model-Checking Algorithms for Continuous-Time Markov Chains, IEEE Transactions on Software Engineering, v.29 n.6, p.524-541, June 2003  [doi>10.1109/TSE.2003.1205180]
 	
3Berberian, S. K. 1998. Fundamentals of Real Analysis. Springer.
 	
4Bialas, J. 1990. The σ-additive measure theory. J. Formal. Math. 2.
 	
5Bogachev, V. I. 2006. Measure Theory. Springer.
 	
6D. Chaum, The dining cryptographers problem: unconditional sender and recipient untraceability, Journal of Cryptology, v.1 n.1, p.65-75, 1988
 	
7Coble, A. R. 2010. Anonymity, information, and machine-assisted proof. Ph.D. thesis, University of Cambridge.
 
8Thomas M. Cover , Joy A. Thomas, Elements of information theory, Wiley-Interscience, New York, NY, 1991
 	
9de Alfaro, L. 1997. Ph.D. thesis, Stanford University.
 	
10Fraenkel, A., Bar-Hillel, Y., and Levy, A. 1973. Foundations of Set Theory. North Holland.
 	
11Michael J. C. Gordon, Mechanizing programming logics in higher order logic, Current trends in hardware verification and automated theorem proving, Springer-Verlag New York, Inc., New York, NY, 1989
 	
12M. J. C. Gordon , T. F. Melham, Introduction to HOL: a theorem proving environment for higher order logic, Cambridge University Press, New York, NY, 1993
 	
13Halmos, P. R. 1944. The foundations of probability. Amer. Math. Monthly 51, 9, 493--510.
 	
14John Harrison, Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, New York, NY, 2009
 	
15Osman Hasan , Sofiène Tahar, Verification of expectation properties for discrete random variables in HOL, Proceedings of the 20th international conference on Theorem proving in higher order logics, p.119-134, September 10-13, 2007, Kaiserslautern, Germany
 	
16Hasan, O. and Tahar, S. 2009a. Formal verification of tail distribution bounds in the HOL theorem prover. Math. Methods Appl. Sci. 32, 4 (March), 480--504.
 	
17Osman Hasan , Sofiène Tahar, Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL, Journal of Automated Reasoning, v.42 n.1, p.1-33, January 2009  [doi>10.1007/s10817-008-9105-6]
 	
18Osman Hasan , Naeem Abbasi , Behzad Akbarpour , Sofiène Tahar , Reza Akbarpour, Formal Reasoning about Expectation Properties for Continuous Random Variables, Proceedings of the 2nd World Congress on Formal Methods, November 02-06, 2009, Eindhoven, The Netherlands  [doi>10.1007/978-3-642-05089-3_28]
 	
19Osman Hasan , Sofiene Tahar , Naeem Abbasi, Formal Reliability Analysis Using Theorem Proving, IEEE Transactions on Computers, v.59 n.5, p.579-592, May 2010  [doi>10.1109/TC.2009.165]
 	
20Hurd, J. 2002. Formal verifcation of probabilistic algorithms. Ph.D. thesis, University of Cambridge.
 	
21Marta Kwiatkowska , Gethin Norman , David Parker, Quantitative Analysis With the Probabilistic Model Checker PRISM, Electronic Notes in Theoretical Computer Science (ENTCS), v.153 n.2, p.5-31, May, 2006  [doi>10.1016/j.entcs.2005.10.030]
	
22David R Lester, Topology in PVS: continuous mathematics with applications, Proceedings of the second workshop on Automated formal methods, p.11-20, November 06-06, 2007, Atlanta, Georgia  [doi>10.1145/1345169.1345171]
 	
23Mhamdi, T., Hasan, O., and Tahar, S. 2010a. Formal analysis of systems with probabilistic behavior in HOL. http://users.encs.concordia.ca/~mhamdi/hol/probability/.
 	
24Tarek Mhamdi , Osman Hasan , Sofiène Tahar, On the formalization of the lebesgue integration theory in HOL, Proceedings of the First international conference on Interactive Theorem Proving, July 11-14, 2010, Edinburgh, UK  [doi>10.1007/978-3-642-14052-5_27]
 	
25Nȩdzusiak, A. 1989. σ-fields and Probability. J. Formal. Math. 1.
 	
26Sam Owre , John M. Rushby , Natarajan Shankar, PVS: A Prototype Verification System, Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, p.748-752, June 15-18, 1992
 	
27Papoulis, A. 1984. Probability, Random Variables, and Stochastic Processes. Mc-Graw Hill.
 	
28Parker, D. 2001. Ph.D. thesis, University of Birmingham, Birmingham, UK.
 	
29Paulson, L. C. 1994. Isabelle: A Generic Theorem Prover. Springer.
	
30Michael K. Reiter , Aviel D. Rubin, Crowds: anonymity for Web transactions, ACM Transactions on Information and System Security (TISSEC), v.1 n.1, p.66-92, Nov. 1998  [doi>10.1145/290163.290168]
 	
31Richter, S. 2004. Formalizing integration theory with an application to probabilistic algorithms. In Proceedings of the 17the International Conference on Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science. vol. 3223. 271--286.
 	
32Rutten, J., Kwaiatkowska, M., Normal, G., and Parker, D. 2004. Mathematical Techniques for Analyzing Concurrent and Probabilisitc Systems. CRM Monograph Series, vol. 23. American Mathematical Society.
 	
33Koushik Sen , Mahesh Viswanathan , Gul Agha, VESTA: A Statistical Model-checker and Analyzer for Probabilistic Systems, Proceedings of the Second International Conference on the Quantitative Evaluation of Systems, p.251, September 19-22, 2005  [doi>10.1109/QEST.2005.42]
 	
34Geoffrey Smith, On the Foundations of Quantitative Information Flow, Proceedings of the 12th International Conference on Foundations of Software Science and Computational Structures: Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, March 22-29, 2009, York, UK  [doi>10.1007/978-3-642-00596-1_21]
 	
35Wagon, S. 1993. The Banach-Tarski Paradox. Cambridge University Press.