CADE-22: Tutorial

22nd International Conference on Automated Deduction
McGill University, Montreal, Canada
August 2 - 7, 2009

 Probabilistic Analysis using a Theorem Prover

Time: August 2, 2009 (Morning Session)
Location: McGill University, Montreal, Canada

Organizers: Osman Hasan and Sofiene Tahar
Organizer Affiliation: Department of Electrical and Computer Engineering, Concordia University, Montreal, Canada



Hardware and software systems usually exhibit some random or unpredictable elements. Examples include failures due to environmental conditions or aging phenomena in hardware components and the execution of certain actions based on a probabilistic choice in randomized algorithms. Moreover, these systems act upon and within complex environments that themselves have certain elements of unpredictability, such as noise effects in hardware components and the unpredictable traffic pattern in the case of telecommunication protocols. Due to these random components, establishing the correctness of a system under all circumstances usually becomes impractically expensive. The engineering approach to analyze a system with these kind of unavoidable elements of randomness and uncertainty is to use probabilistic analysis. Even for hardware and software systems for which correctness may be unconditionally guaranteed, the study of system performance primarily relies on probabilistic analysis. In fact, the term system performance commonly refers to the average time required by a system to perform a given task, such as the average runtime of a computational algorithm or the average message delay of a telecommunication protocol. These averages can be computed, based on a probabilistic analysis approach, by using appropriate random variables to model inputs for the system model. 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. This unreliable nature of the results poses a serious problem in safety critical applications, such as those in space travel, military, and medicine. A possible solution for overcoming these limitations is to conduct probabilistic analysis within the sound core of a higher-order-logic theorem prover. Due to the high expressiveness of the higher-order logic and the inherent soundness of interactive theorem proving, this approach can be used to conduct error free probabilistic analysis of any system, which can be expressed mathematically, at the cost of significant user interaction.

There have been some recent developments related to the automated reasoning of probabilistic notions, such as the formalization of both discrete [1] and continuous [2,3] random variables in higher-order-logic and the verification of their corresponding probabilistic [4] and statistical properties [5,6,7] in a theorem prover. We believe that by utilizing these capabilities, we can handle the higher-order-logic theorem proving based probabilistic analysis of a variety of hardware and software systems with reasonable amount of modeling and verification efforts. The main idea, illustrated in the figure below, is to construct higher-order-logic models of systems while representing their random components by appropriate formalized discrete and continuous random variables. The probabilistic and statistical characteristics of the system can then be formally reasoned about in a theorem prover using the probability distribution functions, such as probability mass function (PMF) and cumulative distribution function (CDF), and statistical quantities, like mean and variance, of the random variables used in its model.

The above infrastructure has been successfully used for the analysis of the Coupon Collector's problem [7], the automated repeat request (ARQ) communication protocols [8], the Stop-and-Wait protocol [9], the ARQ mechanism at the logic link control (LLC) layer of the General Packet Radio Service (GPRS) [10] and the repairability condition of hardware reconfigurable memory arrays in the presence of stuck-at faults [11]. The main focus of the tutorial is to introduce the above mentioned higher-order-logic formalizations of probability theory concepts and present their practical effectiveness for conducting precise probabilistic analysis of real world hardware and software systems. The tutorial is organized as follows:


Osman Hasan: o_hasan AT ece DOT concordia DOT ca
Sofiene Tahar: tahar AT ece DOT concordia DOT ca


[1] J. Hurd. Formal Verification of Probabilistic Algorithms. PhD Thesis, University of Cambridge, Cambridge, UK, 2002.

[2] O.Hasan and S. Tahar. Formalization of the Standard Uniform Random Variable. Theoretical Computer ScienceVol. 382, No. 1, Elsevier B.V. Pub., 2007, pages 71-83.

[3] 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.]

[4] 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.]

[5] 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.]

[6] O.Hasan and S. Tahar. Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables. Journal of Automated Reasoning, Springer Verlag, Vol. 41, No. 3-4, Springer Verlag, November 2008, pp. 295-323.

[7] O.Hasan and S. Tahar. Formal Verification of Tail Distribution Bounds in the HOL Theorem Prover. Mathematical Methods in the Applied Sciences, Wiley InterScience, Vol. 32, no. 4, Wiley Interscience, March 2009, pp. 480-504.

[8] 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.

[9] O.Hasan and S. Tahar. Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL. Journal of Automated Reasoning, Springer Verlag, Vol. 42, No. 1, Springer Verlag, January 2009, pp. 1-33.

[10] 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.

[11] 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), Düsseldorf, Germany, February 2009.]

Last Updated: July 9, 2009.