Probabilistic analysis is a tool of fundamental importance to virtually all scientists and engineers as they often have to deal with systems that exhibit random or unpredictable elements. Traditionally, computer simulation techniques are used to perform probabilistic analysis. However, they provide less accurate results and cannot handle large-scale problems due to their enormous computer processing time requirements. To overcome these limitations, we propose to perform probabilistic analysis by formally specifying the behavior of random systems in higher-order logic and use these models for verifying the intended probabilistic and statistical properties in a computer based theorem prover. The analysis carried out in this way is free from any approximation or precision issues due to the mathematical nature of the models and the inherent soundness of the theorem proving approach.


We mainly target the two most essential components for this task, i.e., the higher-order-logic formalization of random \variables and the ability to formally verify the probabilistic and statistical properties of these random variables within a theorem prover. We present a framework that can be used to formalize and \verify any continuous random variable for which the inverse of the cumulative distribution function can be expressed in\ a closed mathematical form. Similarly, we provide a formalization infrastructure that allows us to reason about statis\tical properties, such as mean or variance and tail distribution bounds, for discrete random variables. All the above m\entioned work is conducted using the HOL theorem prover. Finally, in order to illustrate the practical effectiveness of\ the proposed approach, we consider the probabilistic analysis of three examples: the Coupon Collector's problem, the r\oundoff error in a digital processor and the Stop-and-Wait protocol.

Journal Papers

1. O. Hasan, S. Tahar, N. Abassi: Formal Reliability Analysis using Theorem Proving, IEEE Transactions on Computers, DOI:10.1109/TC.2009.165, 23 Oct. 2009, pp. 1-14.
2. O. Hasan and S. Tahar: Probabilistic Analysis of Wireless Systems using Theorem Proving; Electronic Notes in Theoretical Computer Science, Vol. 242, No. 2, Elsevier B.V. Pub., July 2009, pp. 43-58.
3. O.Hasan and S. Tahar: Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables. Journal of Automated Reasoning, Vol. 41, No. 3-4, Springer Verlag, November 2008, pp. 295-323.
4. O.Hasan and S. Tahar: Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL. Journal of Automated Reasoning, Vol. 42, No. 1, Springer Verlag, January 2009, pp. 1-33.
5. O.Hasan and S. Tahar: Formal Verification of Tail Distribution Bounds in the HOL Theorem Prover. Mathematical Methods in The Applied Sciences, Vol. 32, no. 4, Wiley Interscience, March 2009, pp. 480-504.
6. O.Hasan and S. Tahar: Formalization of the Standard Uniform Random Variable. Theoretical Computer Science, Vol. 382, No. 1, Elsevier B.V. Pub., 2007, pages 71-83.

Conference Papers

1. O. Hasan, N. Abbasi, B. Akbarpour, S. Tahar, and R. Akbarpour: Formal Reasoning about Expectation Properties for Continuous Random Variables; In: A. Cavalcanti and D. Dams (Eds.), Formal Methods, Lecture Notes in Computer Science 5850, Springer Verlag, 2009, pp. 435-450. [Proc. International Symposium on Formal Methods (FM'09) , Eindhoven, The Netherlands, November 2009.]
2. O. Hasan, N. Abbasi and S. Tahar: Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays; In: M. Leuschel and H. Wehrheim (Eds.), Integrated Formal Methods, Lecture Notes in Computer Science 5423, Springer Verlag, 2009, pp. 277-291. [Proc. International Conference on Integrated Formal Methods (IFM'09), DC
3. O. Hasan and S. Tahar: Performance Analysis of Wireless Systems using Theorem Proving; In: Jens Chr. Godskesen and Massimo Merro (Eds.), First International Workshop on Formal Methods for Wireless Systems (FMWS'2008), Toronto, ON, Canada, August 2008, pp. 3-18, ISSN 1600-6100, ISBN 978-87-7949-183-0.
4. O. Hasan. Probabilistic Analysis using Theorem Proving; In: O. Ait Mohammed, C. Munoz and S. Tahar (Eds.) International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'08), Emerging Trend Proceedings, Montreal, QC, Canada, August 2008, pp. 21-33.
5. O. Hasan and S. Tahar: Performance Analysis of ARQ Protocols using a Theorem Prover; In IEEE International Symposium on Performance Analysis of Systems and Software (ISPASS'08), IEEE Computer Society, Austin, Texas, USA, April 2008, pp. 85-94.
6. O. Hasan and S. Tahar: Verification of Tail Distribution Bounds in a Theorem Prover; In: T.E.Simos, G. Psihoyios and Ch. Tsitouras (Eds.), Numerical Analysis and Applied Mathematics, AIP Conference Proceedings Volume 936, 2007, pp. 259-262. [Proc. International Conference of Numerical Analysis and Applied Mathematics (ICNAAM'07), Corfu, Greece, September 2007.]
7. O. Hasan and S. Tahar: Verification of Expectation Properties for Discrete Random Variables in HOL; In: K.Schneider and J.Brandt (Eds.), Theorem Proving in Higher-Order Logics, Lecture Notes in Computer Science 4732, Springer Verlag, 2007, pp. 119-134. [Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'07), Kaiserslautern, Germany, September 2007.]
8. O.Hasan and S. Kort. Automated Formal Synthesis of Wallace Tree Multipliers. In 50th IEEE Int'l Midwest Symposium on Circuits & Systems, pages 293-296. Montreal, Canada, August 2007.
9. O. Hasan and S. Tahar: Formalization of Continuous Probability Distributions; In: F. Pfenning (Ed.), Automated Deduction, Lecture Notes in Computer Science 4603, Springer Verlag, 2007, pp. 2-18. [Proc. 21st Conference on Automated Deduction (CADE-21), Bremen, Germany, July 2007.]
10. O. Hasan and S. Tahar: Verification of Probabilistic Properties in the HOL Theorem Prover; In: J. Davies and J. Gibbons (Eds.), Integrated Formal Methods, Lecture Notes in Computer Science 4591, Springer Verlag, 2007, pp. 333-352. [Proc. International Conference on Integrated Formal Methods (IFM'07), Oxford, UK, July 2007.]

Technical Reports

1. O. Hasan and S. Tahar: Formal Verification of Expectation and Variance for Discrete Random Variables; Technical Report, Concordia University, Department of Electrical and Computer Engineering, June 2007. [27 pages]
2. O.Hasan and S. Tahar: Formalization of Continuous Probability Distributions; Technical Report, Concordia University, Department of Electrical and Computer Engineering, February 2007. [42 pages]
3. O.Hasan and S. Tahar: Standard Uniform Distribution Theory in HOL-4; Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 2006. [14 pages]
4. O.Hasan and S. Tahar: Formalization of the Standard Uniform Random Variable in HOL; Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 2006. [20 pages]

Thesis
O.Hasan. Formal Probabilistic Analysis using Theorem Proving. Concordia University, Montreal, Canada. April 2008.